1 /-
2 Copyright (c) 2018 Johannes Hölzl. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Johannes Hölzl, Jens Wagemaker
5
6 Theory of unique factorization domains.
7
8 @TODO: setup the complete lattice structure on `factor_set`.
9 -/
10 import algebra.gcd_domain
src └────────────────┘
11
12 variables {α : Type*}
id ┴
typ ┴
13 local infix ` ~ᵤ ` : 50 := associated
id └────────┘
src └────────┘
typ └────────┘
14
15 /-- Unique factorization domains.
16
17 In a unique factorization domain each element (except zero) is uniquely
18 represented as a multiset of irreducible factors.
19 Uniqueness is only up to associated elements.
20
21 This is equivalent to defining a unique factorization domain as a domain in
22 which each element (except zero) is non-uniquely represented as a multiset
23 of prime factors. This definition is used.
24
25 To define a UFD using the traditional definition in terms of multisets
26 of irreducible factors, use the definition `of_unique_irreducible_factorization`
27
28 -/
29 class unique_factorization_domain (α : Type*) [integral_domain α] :=
id └───┘ └─────────────┘ ┴
src └─────────────┘
typ └───┘ └─────────────┘ ┴
30 (factors : α → multiset α)
id ┴ ┴ └──────┘ ┴
src └──────┘
typ ┴ ┴ └──────┘ ┴
doc └──────┘
31 (factors_prod : ∀{a : α}, a ≠ 0 → (factors a).prod ~ᵤ a)
id ┴ ┴ ┴ ┴ └─────┘ ┴ └──┘ └┘ ┴
src ┴ └──┘ └┘
typ ┴ ┴ ┴ ┴ └─────┘ ┴ └──┘ └┘ ┴
doc └──┘
32 (prime_factors : ∀{a : α}, a ≠ 0 → ∀x∈factors a, prime x)
id ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └───┘ ┴
src ┴ ┴ └───┘
typ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └───┘ ┴
doc └───┘
33
34 namespace unique_factorization_domain
35
36 variables [integral_domain α] [unique_factorization_domain α]
id └─────────────┘ └─────────────────────────┘
src └─────────────┘ └─────────────────────────┘
typ └─────────────┘ └─────────────────────────┘
doc └─────────────────────────┘
37
38 @[elab_as_eliminator] lemma induction_on_prime {P : α → Prop}
id ┴
typ ┴
doc └────────────────┘
39 (a : α) (h₁ : P 0) (h₂ : ∀ x : α, is_unit x → P x)
id ┴ ┴ ┴ └─────┘ ┴ ┴ ┴
src └─────┘
typ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘
40 (h₃ : ∀ a p : α, a ≠ 0 → prime p → P a → P (p * a)) : P a :=
id ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴
typ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘
41 by haveI := classical.dec_eq α; exact
id └──────────────┘ ┴
src └───────┘└──────────────┘┴ └────┘
typ └───────┘└──────────────┘┴┴ └────┘
doc └───────┘ ┴ └────┘
txt └───────┘ ┴ └────┘
par └───────┘ ┴ └────┘
pid ┴└─┘ ┴ ┴
st └───────────────────────────────────
42 if ha0 : a = 0 then ha0.symm ▸ h₁
id └┘ ┴ └───┘ ┴ └┘
src └┘└─────┘ ┴┴└──────┘ └───┘┴┴┴ └
typ └┘└─────┘ ┴┴└──────┘ └───┘┴┴┴└┘└
doc └─────┘ ┴ └──────┘ ┴ ┴ └
txt └─────┘ ┴ └──────┘ ┴ ┴ └
par └─────┘ ┴ └──────┘ ┴ ┴ └
pid └─────┘ ┴ └──────┘ ┴ ┴ └
st ──────────────────────────────────
43 else @multiset.induction_on _
id └───────────────────┘
src ────┘ └───────────────────┘└──
typ ────┘ └───────────────────┘└──
doc ────┘ └──
txt ────┘ └──
par ────┘ └──
pid ────┘ └──
st ──────────────────────────────
44 (λ s : multiset α, ∀ (a : α), a ≠ 0 → s.prod ~ᵤ a → (∀ p ∈ s, prime p) → P a)
id └──────┘ ┴ ┴ └───┘ └┘ └───┘ ┴
src ─┘ └───┘└──────┘┴ └┘ └────┘ ┴ ┴ ┴┴└─┘ ┴ └───┘┴└┘┴ ┴ ┴ └───┘ ┴└───┘┴ └┘ └┘ ┴ └─
typ ─┘ └───┘└──────┘┴ └┘ └────┘┴┴ ┴ ┴┴└─┘ ┴ └───┘┴└┘┴ ┴ ┴ └───┘ ┴└───┘┴ └┘ └┘┴┴ └─
doc ─┘ └───┘└──────┘┴ └┘ └────┘ ┴ ┴ ┴ └─┘ ┴ └───┘┴ ┴ ┴ ┴ └───┘ ┴└───┘┴ └┘ └┘ ┴ └─
txt ─┘ └───┘ ┴ └┘ └────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └┘ └┘ ┴ └─
par ─┘ └───┘ ┴ └┘ └────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └┘ └┘ ┴ └─
pid ─┘ └───┘ ┴ └┘ └────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └┘ └┘ ┴ └─
st ─────────────────────────────────────────────────────────────────────────────────
45 (factors a)
id └─────┘ ┴
src ─┘ └─────┘┴ └─
typ ─┘ └─────┘┴┴└─
doc ─┘ ┴ └─
txt ─┘ ┴ └─
par ─┘ ┴ └─
pid ─┘ ┴ └─
st ──────────────
46 (λ _ _ h _, h₂ _ ((is_unit_iff_of_associated h.symm).2 is_unit_one))
id └┘ └───────────────────────┘ └───┘ └─────────┘
src ─┘ └────────┘ └─┘ └───────────────────────┘┴ └───┘└──┘└─────────┘└──
typ ─┘ └────────┘└┘└─┘ └───────────────────────┘┴ └───┘└──┘└─────────┘└──
doc ─┘ └────────┘ └─┘ ┴ └──┘ └──
txt ─┘ └────────┘ └─┘ ┴ └──┘ └──
par ─┘ └────────┘ └─┘ ┴ └──┘ └──
pid ─┘ └────────┘ └─┘ ┴ └──┘ └──
st ───────────────────────────────────────────────────────────────────────
47 (λ p s ih a ha0 ⟨u, hu⟩ hsp,
id ┴
src ─┘ └─────────────┘ └┘ └──────
typ ─┘ └─────────────┘┴└┘ └──────
doc ─┘ └─────────────┘ └┘ └──────
txt ─┘ └─────────────┘ └┘ └──────
par ─┘ └─────────────┘ └┘ └──────
pid ─┘ └─────────────┘ └┘ └──────
st ───────────────────────────────
48 have ha : a = (p * u) * s.prod, by simp [hu.symm, mul_comm, mul_assoc],
id ┴ └───┘ └──────┘ └───────┘
src ───┘ └────┘ ┴ ┴ ┴ ┴ └┘┴┴ └───┘└───┘└────┘ └┘└──────┘└┘└───────┘┴└─
typ ───┘ └────┘ ┴ ┴ ┴ ┴ └┘┴┴ └───┘└───┘└────┘└─────┘└┘└──────┘└┘└───────┘┴└─
doc ───┘ └────┘ ┴ ┴ ┴ ┴ └┘ ┴ └───┘└───┘└────┘ └┘ └┘ ┴└─
txt ───┘ └────┘ ┴ ┴ ┴ ┴ └┘ ┴ └───┘└────┘ └┘ └┘ ┴└─
par ───┘ └────┘ ┴ ┴ ┴ ┴ └┘ ┴ └───┘└────┘ └┘ └┘ ┴└─
pid ───┘ └────┘ ┴ ┴ ┴ ┴ └┘ ┴ └─────────┘ └┘ └┘ └──
st ─────────────────────────────────────┘└──────────────────────────────────┘└─
49 have hs0 : s.prod ≠ 0, from λ _ : s.prod = 0, by simp * at *,
id └───┘ ┴
src ───┘ └─────┘ └───┘┴ └───────┘ └───┘ ┴ └──┘ ┴└─────────┘└─
typ ───┘ └─────┘ └───┘┴ └───────┘ └───┘ ┴┴└──┘ ┴└─────────┘└─
doc ───┘ └─────┘ └───┘┴ └───────┘ └───┘ ┴ └──┘ ┴└─────────┘└─
txt ───┘ └─────┘ ┴ └───────┘ └───┘ ┴ └──┘ ┴└─────────┘└─
par ───┘ └─────┘ ┴ └───────┘ └───┘ ┴ └──┘ ┴└─────────┘└─
pid ───┘ └─────┘ ┴ └───────┘ └───┘ ┴ └──┘ └─────────────
st ───────────────────────────────────────────────────┘└──────────┘└─
50 ha.symm ▸ h₃ _ _ hs0
id └┘
src ───┘ ┴ ┴ └───┘ └
typ ───┘ ┴ ┴└┘└───┘ └
doc ───┘ ┴ ┴ └───┘ └
txt ───┘ ┴ ┴ └───┘ └
par ───┘ ┴ ┴ └───┘ └
pid ───┘ ┴ ┴ └───┘ └
st ─────────────────────────
51 (prime_of_associated ⟨u, rfl⟩ (hsp p (multiset.mem_cons_self _ _)))
id └─────────────────┘ └─┘ ┴ └────────────────────┘
src ─────┘ └─────────────────┘┴ └┘└─┘└┘ ┴ ┴ └────────────────────┘└───────
typ ─────┘ └─────────────────┘┴ └┘└─┘└┘ ┴┴┴ └────────────────────┘└───────
doc ─────┘ ┴ └┘ └┘ ┴ ┴ └───────
txt ─────┘ ┴ └┘ └┘ ┴ ┴ └───────
par ─────┘ ┴ └┘ └┘ ┴ ┴ └───────
pid ─────┘ ┴ └┘ └┘ ┴ ┴ └───────
st ──────────────────────────────────────────────────────────────────────────
52 (ih _ hs0 (by refl) (λ p hp, hsp p (multiset.mem_cons.2 (or.inr hp)))))
id └───────────────┘ └────┘
src ─────┘ └─┘ ┴ ┴└──┘└┘ └─────┘ ┴ ┴ └───────────────┘└─┘ └────┘┴ └─────
typ ─────┘ └─┘ ┴ ┴└──┘└┘ └─────┘ ┴ ┴ └───────────────┘└─┘ └────┘┴ └─────
doc ─────┘ └─┘ ┴ ┴└──┘└┘ └─────┘ ┴ ┴ └─┘ ┴ └─────
txt ─────┘ └─┘ ┴ ┴└──┘└┘ └─────┘ ┴ ┴ └─┘ ┴ └─────
par ─────┘ └─┘ ┴ ┴└──┘└┘ └─────┘ ┴ ┴ └─┘ ┴ └─────
pid ─────┘ └─┘ ┴ └─────┘ └─────┘ ┴ ┴ └─┘ ┴ └─────
st ──────────────────┘└───┘└─────────────────────────────────────────────────────
53 _
src ────
typ ────
doc ────
txt ────
par ────
pid ────
st ────
54 ha0
src ─┘ └
typ ─┘ └
doc ─┘ └
txt ─┘ └
par ─┘ └
pid ─┘ └
st ──────
55 (factors_prod ha0)
id └──────────┘
src ─┘ └──────────┘┴ └─
typ ─┘ └──────────┘┴ └─
doc ─┘ ┴ └─
txt ─┘ ┴ └─
par ─┘ ┴ └─
pid ─┘ ┴ └─
st ─────────────────────
56 (prime_factors ha0)
id └───────────┘
src ─┘ └───────────┘┴ └─
typ ─┘ └───────────┘┴ └─
doc ─┘ ┴ └─
txt ─┘ ┴ └─
par ─┘ ┴ └─
pid ─┘ ┴ ┴└
st ──────────────────────
57
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
58 lemma factors_irreducible {a : α} (ha : irreducible a) :
id ┴ └─────────┘ ┴
src └─────────┘
typ ┴ └─────────┘ ┴
doc └─────────┘
59 ∃ p, a ~ᵤ p ∧ factors a = p :: 0 :=
id ┴ ┴┴ ┴ └┘ ┴ ┴ └─────┘ ┴ ┴ ┴ └┘
src ┴ ┴ └┘ ┴ └─────┘ ┴ └┘
typ ┴ ┴┴ ┴ └┘ ┴ ┴ └─────┘ ┴ ┴ ┴ └┘
doc └┘
60 by haveI := classical.dec_eq α; exact
id └──────────────┘ ┴
src └───────┘└──────────────┘┴ └────┘
typ └───────┘└──────────────┘┴┴ └────┘
doc └───────┘ ┴ └────┘
txt └───────┘ ┴ └────┘
par └───────┘ ┴ └────┘
pid ┴└─┘ ┴ ┴
st └───────────────────────────────────
61 multiset.induction_on (factors a)
id └───────────────────┘ └─────┘ ┴
src └───────────────────┘┴ └─────┘┴ └─
typ └───────────────────┘┴ └─────┘┴┴└─
doc ┴ ┴ └─
txt ┴ ┴ └─
par ┴ ┴ └─
pid ┴ ┴ └─
st ──────────────────────────────────
62 (λ h, (ha.1 (associated_one_iff_is_unit.1 h.symm)).elim)
id └────────────────────────┘ └───┘
src ─┘ └──┘ └─┘ └────────────────────────┘└─┘ └───┘└────────
typ ─┘ └──┘ └─┘ └────────────────────────┘└─┘ └───┘└────────
doc ─┘ └──┘ └─┘ └─┘ └────────
txt ─┘ └──┘ └─┘ └─┘ └────────
par ─┘ └──┘ └─┘ └─┘ └────────
pid ─┘ └──┘ └─┘ └─┘ └────────
st ───────────────────────────────────────────────────────────
63 (λ p s _ hp hs, let ⟨u, hu⟩ := hp in ⟨p,
id ┴
src ─┘ └────────────┘ ┴ └┘ └───┘ └──┘ └─
typ ─┘ └────────────┘ ┴ ┴└┘ └───┘ └──┘ └─
doc ─┘ └────────────┘ ┴ └┘ └───┘ └──┘ └─
txt ─┘ └────────────┘ ┴ └┘ └───┘ └──┘ └─
par ─┘ └────────────┘ ┴ └┘ └───┘ └──┘ └─
pid ─┘ └────────────┘ ┴ └┘ └───┘ └──┘ └─
st ───────────────────────────────────────────
64 have hs0 : s = 0, from classical.by_contradiction
id ┴ └────────────────────────┘
src ───┘ └─────┘ ┴┴└───────┘└────────────────────────┘└
typ ───┘ └─────┘ ┴┴└───────┘└────────────────────────┘└
doc ───┘ └─────┘ ┴ └───────┘ └
txt ───┘ └─────┘ ┴ └───────┘ └
par ───┘ └─────┘ ┴ └───────┘ └
pid ───┘ └─────┘ ┴ └───────┘ └
st ──────────────────────────────────────────────────────
65 (λ hs0, let ⟨q, hq⟩ := multiset.exists_mem_of_ne_zero hs0 in
id ┴ └────────────────────────────┘
src ─────┘ └────┘ ┴ └┘ └───┘└────────────────────────────┘┴ └───
typ ─────┘ └────┘ ┴ ┴└┘ └───┘└────────────────────────────┘┴ └───
doc ─────┘ └────┘ ┴ └┘ └───┘ ┴ └───
txt ─────┘ └────┘ ┴ └┘ └───┘ ┴ └───
par ─────┘ └────┘ ┴ └┘ └───┘ ┴ └───
pid ─────┘ └────┘ ┴ └┘ └───┘ ┴ └───
st ───────────────────────────────────────────────────────────────────
66 (hs q (by simp [hq])).2.1 $
id └┘
src ──────┘ ┴ ┴ ┴└────┘ ┴└─────┘ └
typ ──────┘ ┴ ┴ ┴└────┘└┘┴└─────┘ └
doc ──────┘ ┴ ┴ ┴└────┘ ┴└─────┘ └
txt ──────┘ ┴ ┴ ┴└────┘ ┴└─────┘ └
par ──────┘ ┴ ┴ ┴└────┘ ┴└─────┘ └
pid ──────┘ ┴ ┴ └─────┘ └──────┘ └
st ───────────────┘└────────┘└────────
67 (ha.2 ((p * u) * (s.erase q).prod) _
id ┴ ┴ ┴└────┘
src ───────┘ └─┘ ┴ ┴ └┘┴┴ └────┘┴ └─────────
typ ───────┘ └─┘ ┴┴ ┴ └┘┴┴ ┴└────┘┴ └─────────
doc ───────┘ └─┘ ┴ ┴ └┘ ┴ └────┘┴ └─────────
txt ───────┘ └─┘ ┴ ┴ └┘ ┴ ┴ └─────────
par ───────┘ └─┘ ┴ ┴ └┘ ┴ ┴ └─────────
pid ───────┘ └─┘ ┴ ┴ └┘ ┴ ┴ └─────────
st ─────────────────────────────────────────────
68 (by rw [mul_right_comm _ _ q, mul_assoc, ← multiset.prod_cons,
id └────────────┘ ┴ └───────┘ └────────────────┘
src ─────────┘ ┴└──┘└────────────┘└───┘ └┘└───────┘└──┘└────────────────┘└─
typ ─────────┘ ┴└──┘└────────────┘└───┘┴└┘└───────┘└──┘└────────────────┘└─
doc ─────────┘ ┴└──┘ └───┘ └┘ └──┘ └─
txt ─────────┘ ┴└──┘ └───┘ └┘ └──┘ └─
par ─────────┘ ┴└──┘ └───┘ └┘ └──┘ └─
pid ─────────┘ └───┘ └───┘ └┘ └──┘ └─
st ────────────┘└───────────────────────┘└─────────┘└────────────────────┘└─
69 multiset.cons_erase hq]; simp [hu.symm, mul_comm, mul_assoc])).resolve_left $
id └─────────────────┘ └┘ └──────┘ └───────┘
src ───────────┘└─────────────────┘┴ ┴└┘└────┘ └┘└──────┘└┘└───────┘┴└──────────────┘ └
typ ───────────┘└─────────────────┘┴└┘┴└┘└────┘└─────┘└┘└──────┘└┘└───────┘┴└──────────────┘ └
doc ───────────┘ ┴ ┴└┘└────┘ └┘ └┘ ┴└──────────────┘ └
txt ───────────┘ ┴ ┴└┘└────┘ └┘ └┘ ┴└──────────────┘ └
par ───────────┘ ┴ ┴└┘└────┘ └┘ └┘ ┴└──────────────┘ └
pid ───────────┘ ┴ └───────┘ └┘ └┘ └───────────────┘ └
st ─────────────────────────────────┘┴└───────────────────────────────────┘└─────────────────
70 mt is_unit_of_mul_is_unit_left $ mt is_unit_of_mul_is_unit_left
id └┘ └─────────────────────────┘
src ─────────────┘ ┴ ┴ ┴└┘┴└─────────────────────────┘└
typ ─────────────┘ ┴ ┴ ┴└┘┴└─────────────────────────┘└
doc ─────────────┘ ┴ ┴ ┴ ┴ └
txt ─────────────┘ ┴ ┴ ┴ ┴ └
par ─────────────┘ ┴ ┴ ┴ ┴ └
pid ─────────────┘ ┴ ┴ ┴ ┴ └
st ──────────────────────────────────────────────────────────────────────────────
71 (hs p (multiset.mem_cons_self _ _)).2.1),
id └────────────────────┘
src ───────────────┘ ┴ ┴ └────────────────────┘└────────────
typ ───────────────┘ ┴ ┴ └────────────────────┘└────────────
doc ───────────────┘ ┴ ┴ └────────────
txt ───────────────┘ ┴ ┴ └────────────
par ───────────────┘ ┴ ┴ └────────────
pid ───────────────┘ ┴ ┴ └────────────
st ──────────────────────────────────────────────────────────
72 ⟨associated.symm (by clear _let_match; simp * at *), hs0 ▸ rfl⟩⟩)
id └─────────────┘ ┴ └─┘
src ───┘ └─────────────┘┴ ┴└──────────────┘└┘└─────────┘└─┘ ┴┴┴└─┘└───
typ ───┘ └─────────────┘┴ ┴└──────────────┘└┘└─────────┘└─┘ ┴┴┴└─┘└───
doc ───┘ ┴ ┴└──────────────┘└┘└─────────┘└─┘ ┴ ┴ └───
txt ───┘ ┴ ┴└──────────────┘└┘└─────────┘└─┘ ┴ ┴ └───
par ───┘ ┴ ┴└──────────────┘└┘└─────────┘└─┘ ┴ ┴ └───
pid ───┘ ┴ └───────────────────────────────┘ ┴ ┴ └───
st ───────────────────────┘└────────────────────────────┘└───────────────
73 (factors_prod ha.ne_zero)
id └──────────┘
src ─┘ └──────────┘┴ └─
typ ─┘ └──────────┘┴ └─
doc ─┘ ┴ └─
txt ─┘ ┴ └─
par ─┘ ┴ └─
pid ─┘ ┴ └─
st ────────────────────────────
74 (prime_factors ha.ne_zero)
id └───────────┘ └────────┘
src ─┘ └───────────┘┴└────────┘└─
typ ─┘ └───────────┘┴└────────┘└─
doc ─┘ ┴ └─
txt ─┘ ┴ └─
par ─┘ ┴ └─
pid ─┘ ┴ ┴└
st ─────────────────────────────
75
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
76 lemma irreducible_iff_prime {p : α} : irreducible p ↔ prime p :=
id ┴ └─────────┘ ┴ ┴ └───┘ ┴
src └─────────┘ ┴ └───┘
typ ┴ └─────────┘ ┴ ┴ └───┘ ┴
doc └─────────┘ └───┘
77 by letI := classical.dec_eq α; exact
id └──────────────┘ ┴
src └──────┘└──────────────┘┴ └────┘
typ └──────┘└──────────────┘┴┴ └────┘
doc └──────┘ ┴ └────┘
txt └──────┘ ┴ └────┘
par └──────┘ ┴ └────┘
pid ┴└─┘ ┴ ┴
st └──────────────────────────────────
78 if hp0 : p = 0 then by simp [hp0]
id └┘ ┴ └─┘
src └┘└─────┘ ┴┴└──────┘ ┴└────┘ └┘
typ └┘└─────┘ ┴┴└──────┘ ┴└────┘└─┘└┘
doc └─────┘ ┴ └──────┘ ┴└────┘ └┘
txt └─────┘ ┴ └──────┘ ┴└────┘ └┘
par └─────┘ ┴ └──────┘ ┴└────┘ └┘
pid └─────┘ ┴ └──────┘ └─────┘ └─
st ─────────────────────┘└──────────┘
79 else
src └────
typ └────
doc └────
txt └────
par └────
pid ─────
st └────
80 ⟨λ h, let ⟨q, hq⟩ := factors_irreducible h in
id ┴ ┴ └┘ └─────────────────┘
src ─┘ └──┘ ┴ └┘ └───┘└─────────────────┘┴ └───
typ ─┘┴ └──┘ ┴ ┴└┘└┘└───┘└─────────────────┘┴ └───
doc ─┘ └──┘ ┴ └┘ └───┘ ┴ └───
txt ─┘ └──┘ ┴ └┘ └───┘ ┴ └───
par ─┘ └──┘ ┴ └┘ └───┘ ┴ └───
pid ─┘ └──┘ ┴ └┘ └───┘ ┴ └───
st ────────────────────────────────────────────────
81 have prime q, from hq.2 ▸ prime_factors hp0 _ (by simp [hq.2]),
id └───────────┘ └┘
src ─────┘ └─────┘ └─────┘ └─┘ ┴└───────────┘┴ └─┘ ┴└────┘ └─┘└──
typ ─────┘ └─────┘ └─────┘ └─┘ ┴└───────────┘┴ └─┘ ┴└────┘└┘└─┘└──
doc ─────┘ └─────┘ └─────┘ └─┘ ┴ ┴ └─┘ ┴└────┘ └─┘└──
txt ─────┘ └─────┘ └─────┘ └─┘ ┴ ┴ └─┘ ┴└────┘ └─┘└──
par ─────┘ └─────┘ └─────┘ └─┘ ┴ ┴ └─┘ ┴└────┘ └─┘└──
pid ─────┘ └─────┘ └─────┘ └─┘ ┴ ┴ └─┘ └─────┘ └─────
st ──────────────────────────────────────────────────────┘└──────────┘└──
82 suffices prime (factors p).prod,
id └─────┘ ┴
src ─────┘ └─────┘ └─────┘┴ └───────
typ ─────┘ └─────┘ └─────┘┴┴└───────
doc ─────┘ └─────┘ ┴ └───────
txt ─────┘ └─────┘ ┴ └───────
par ─────┘ └─────┘ ┴ └───────
pid ─────┘ └─────┘ ┴ └───────
st ───────────────────────────────────────
83 from prime_of_associated (factors_prod hp0) this,
id └─────────────────┘ └──────────┘
src ────────────┘└─────────────────┘┴ └──────────┘┴ └┘ └─
typ ────────────┘└─────────────────┘┴ └──────────┘┴ └┘ └─
doc ────────────┘ ┴ ┴ └┘ └─
txt ────────────┘ ┴ ┴ └┘ └─
par ────────────┘ ┴ ┴ └┘ └─
pid ────────────┘ ┴ ┴ └┘ └─
st ──────────────────────────────────────────────────────────
84 hq.2.symm ▸ by simp [this],
id ┴ └──┘
src ─────┘ └──────┘┴┴ ┴└────┘ ┴└─
typ ─────┘ └──────┘┴┴ ┴└────┘└──┘┴└─
doc ─────┘ └──────┘ ┴ ┴└────┘ ┴└─
txt ─────┘ └──────┘ ┴ ┴└────┘ ┴└─
par ─────┘ └──────┘ ┴ ┴└────┘ ┴└─
pid ─────┘ └──────┘ ┴ └─────┘ └──
st ───────────────────┘└──────────┘└─
85 irreducible_of_prime⟩
id └──────────────────┘
src ───┘└──────────────────┘└─
typ ───┘└──────────────────┘└─
doc ───┘ └─
txt ───┘ └─
par ───┘ └─
pid ───┘ ┴└
st ──────────────────────────
86
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
87 lemma irreducible_factors : ∀{a : α}, a ≠ 0 → ∀x∈factors a, irreducible x :=
id ┴ ┴ ┴ ┴ └─────┘ ┴ └─────────┘ ┴
src ┴ └─────┘ └─────────┘
typ ┴ ┴ ┴ ┴ └─────┘ ┴ └─────────┘ ┴
doc └─────────┘
88 by simp only [irreducible_iff_prime]; exact @prime_factors _ _ _
id └───────────────────┘ └───────────┘
src └─────────┘└───────────────────┘┴ └────┘ └───────────┘└──────
typ └─────────┘└───────────────────┘┴ └────┘ └───────────┘└──────
doc └─────────┘ ┴ └────┘ └──────
txt └─────────┘ ┴ └────┘ └──────
par └─────────┘ ┴ └────┘ └──────
pid ┴└──┘└┘ ┴ ┴ └────┘└
st └──────────────────────────────────────────────────────────────
89
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
90 lemma unique : ∀{f g : multiset α},
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
doc └──────┘
91 (∀x∈f, irreducible x) → (∀x∈g, irreducible x) → f.prod ~ᵤ g.prod →
id ┴ ┴ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴└───┘ └┘ ┴└───┘
src └─────────┘ └─────────┘ └───┘ └┘ └───┘
typ ┴ ┴ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴└───┘ └┘ ┴└───┘
doc └─────────┘ └─────────┘ └───┘ └───┘
92 multiset.rel associated f g :=
id └──────────┘ └────────┘ ┴ ┴
src └──────────┘ └────────┘
typ └──────────┘ └────────┘ ┴ ┴
doc └──────────┘
93 by haveI := classical.dec_eq α; exact
id └──────────────┘ ┴
src └───────┘└──────────────┘┴ └────┘
typ └───────┘└──────────────┘┴┴ └────┘
doc └───────┘ ┴ └────┘
txt └───────┘ ┴ └────┘
par └───────┘ ┴ └────┘
pid ┴└─┘ ┴ ┴
st └───────────────────────────────────
94 λ f, multiset.induction_on f
id └───────────────────┘
src └──┘└───────────────────┘┴ └
typ └──┘└───────────────────┘┴ └
doc └──┘ ┴ └
txt └──┘ ┴ └
par └──┘ ┴ └
pid └──┘ ┴ └
st ─────────────────────────────
95 (λ g _ hg h,
src ─┘ └──────────
typ ─┘ └──────────
doc ─┘ └──────────
txt ─┘ └──────────
par ─┘ └──────────
pid ─┘ └──────────
st ───────────────
96 multiset.rel_zero_left.2 $
id └────────────────────┘
src ───┘└────────────────────┘└─┘ └
typ ───┘└────────────────────┘└─┘ └
doc ───┘ └─┘ └
txt ───┘ └─┘ └
par ───┘ └─┘ └
pid ───┘ └─┘ └
st ───────────────────────────────
97 multiset.eq_zero_of_forall_not_mem (λ x hx,
id └────────────────────────────────┘
src ─────┘└────────────────────────────────┘┴ └──────
typ ─────┘└────────────────────────────────┘┴ └──────
doc ─────┘ ┴ └──────
txt ─────┘ ┴ └──────
par ─────┘ ┴ └──────
pid ─────┘ ┴ └──────
st ──────────────────────────────────────────────────
98 have is_unit g.prod, by simpa [associated_one_iff_is_unit] using h.symm,
id └───┘ └────────────────────────┘ └────┘
src ───────┘ └───────┘ └───┘└───┘└─────┘└────────────────────────┘└──────┘└────┘└─
typ ───────┘ └───────┘ └───┘└───┘└─────┘└────────────────────────┘└──────┘└────┘└─
doc ───────┘ └───────┘ └───┘└───┘└─────┘ └──────┘ └─
txt ───────┘ └───────┘ └───┘└─────┘ └──────┘ └─
par ───────┘ └───────┘ └───┘└─────┘ └──────┘ └─
pid ───────┘ └───────┘ └──────────┘ └──────┘ └─
st ──────────────────────────────┘└──────────────────────────────────────────────┘└─
99 (hg x hx).1 (is_unit_iff_dvd_one.2 (dvd.trans (multiset.dvd_prod hx)
id └───────┘ └───────────────┘
src ───────┘ ┴ ┴ └──┘ └─┘ └───────┘┴ └───────────────┘┴ └─
typ ───────┘ ┴ ┴ └──┘ └─┘ └───────┘┴ └───────────────┘┴ └─
doc ───────┘ ┴ ┴ └──┘ └─┘ ┴ ┴ └─
txt ───────┘ ┴ ┴ └──┘ └─┘ ┴ ┴ └─
par ───────┘ ┴ ┴ └──┘ └─┘ ┴ ┴ └─
pid ───────┘ ┴ ┴ └──┘ └─┘ ┴ ┴ └─
st ─────────────────────────────────────────────────────────────────────────────
100 (is_unit_iff_dvd_one.1 this)))))
id └─────────────────┘
src ─────────┘ └─────────────────┘└─┘ └─────
typ ─────────┘ └─────────────────┘└─┘ └─────
doc ─────────┘ └─┘ └─────
txt ─────────┘ └─┘ └─────
par ─────────┘ └─┘ └─────
pid ─────────┘ └─┘ └─────
st ───────────────────────────────────────────
101 (λ p f ih g hf hg hfg,
src ─┘ └────────────────────
typ ─┘ └────────────────────
doc ─┘ └────────────────────
txt ─┘ └────────────────────
par ─┘ └────────────────────
pid ─┘ └────────────────────
st ─────────────────────────
102 let ⟨b, hbg, hb⟩ := exists_associated_mem_of_dvd_prod
id └───────────────────────────────┘
src ───┘ ┴ └┘ └┘ └───┘└───────────────────────────────┘└
typ ───┘ ┴ └┘ └┘ └───┘└───────────────────────────────┘└
doc ───┘ ┴ └┘ └┘ └───┘ └
txt ───┘ ┴ └┘ └┘ └───┘ └
par ───┘ ┴ └┘ └┘ └───┘ └
pid ───┘ ┴ └┘ └┘ └───┘ └
st ──────────────────────────────────────────────────────────
103 (irreducible_iff_prime.1 (hf p (by simp)))
src ─────┘ └─┘ ┴ ┴ ┴└──┘└───
typ ─────┘ └─┘ ┴ ┴ ┴└──┘└───
doc ─────┘ └─┘ ┴ ┴ ┴└──┘└───
txt ─────┘ └─┘ ┴ ┴ ┴└──┘└───
par ─────┘ └─┘ ┴ ┴ ┴└──┘└───
pid ─────┘ └─┘ ┴ ┴ └────────
st ───────────────────────────────────────┘└───┘└───
104 (λ q hq, irreducible_iff_prime.1 (hg _ hq)) $
id └───────────────────┘
src ─────┘ └─────┘└───────────────────┘└─┘ └─┘ └─┘ └
typ ─────┘ └─────┘└───────────────────┘└─┘ └─┘ └─┘ └
doc ─────┘ └─────┘ └─┘ └─┘ └─┘ └
txt ─────┘ └─────┘ └─┘ └─┘ └─┘ └
par ─────┘ └─────┘ └─┘ └─┘ └─┘ └
pid ─────┘ └─────┘ └─┘ └─┘ └─┘ └
st ────────────────────────────────────────────────────
105 (dvd_iff_dvd_of_rel_right hfg).1
id └──────────────────────┘
src ───────┘ └──────────────────────┘┴ └───
typ ───────┘ └──────────────────────┘┴ └───
doc ───────┘ ┴ └───
txt ───────┘ ┴ └───
par ───────┘ ┴ └───
pid ───────┘ ┴ └───
st ─────────────────────────────────────────
106 (show p ∣ (p :: f).prod, by simp) in
id ┴ └┘
src ─────────┘ ┴ ┴┴┴ ┴└┘┴ └─────────┘└──┘└────
typ ─────────┘ ┴ ┴┴┴ ┴└┘┴ └─────────┘└──┘└────
doc ─────────┘ ┴ ┴ ┴ ┴└┘┴ └─────────┘└──┘└────
txt ─────────┘ ┴ ┴ ┴ ┴ ┴ └─────────┘└──┘└────
par ─────────┘ ┴ ┴ ┴ ┴ ┴ └─────────┘└──┘└────
pid ─────────┘ ┴ ┴ ┴ ┴ ┴ └───────────────────
st ────────────────────────────────────┘└───┘└────
107 begin
src ───┘ └
typ ───┘ └
doc ───┘ └
txt ───┘ └
par ───┘ └
pid ───┘ └
st ───┘└─────
108 rw ← multiset.cons_erase hbg,
id └─────────────────┘ └─┘
src ─────┘└───┘└─────────────────┘┴ └─
typ ─────┘└───┘└─────────────────┘┴└─┘└─
doc ─────┘└───┘ ┴ └─
txt ─────┘└───┘ ┴ └─
par ─────┘└───┘ ┴ └─
pid ──────────┘ ┴ └─
st ─────────────────────────────────┘└─
109 exact multiset.rel.cons hb (ih (λ q hq, hf _ (by simp [hq]))
id └───────────────┘ └┘ └┘
src ───────────┘└───────────────┘┴ ┴ ┴ └─────┘ └─┘ ┴└────┘ ┴└──
typ ───────────┘└───────────────┘┴ ┴ └┘┴ └─────┘ └─┘ ┴└────┘└┘┴└──
doc ───────────┘ ┴ ┴ ┴ └─────┘ └─┘ ┴└────┘ ┴└──
txt ───────────┘ ┴ ┴ ┴ └─────┘ └─┘ ┴└────┘ ┴└──
par ───────────┘ ┴ ┴ ┴ └─────┘ └─┘ ┴└────┘ ┴└──
pid ───────────┘ ┴ ┴ ┴ └─────┘ └─┘ └─────┘ └───
st ─────────────────────────────────────────────────────┘└────────┘└──
110 (λ q (hq : q ∈ g.erase b), hg q (multiset.mem_of_mem_erase hq))
id ┴ └─────┘ ┴ └┘ └───────────────────────┘
src ───────┘ └───────┘ ┴┴┴└─────┘┴ └─┘ ┴ ┴ └───────────────────────┘┴ └──
typ ───────┘ └───────┘ ┴┴┴└─────┘┴┴└─┘└┘┴ ┴ └───────────────────────┘┴ └──
doc ───────┘ └───────┘ ┴ ┴└─────┘┴ └─┘ ┴ ┴ ┴ └──
txt ───────┘ └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──
par ───────┘ └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──
pid ───────┘ └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──
st ────────────────────────────────────────────────────────────────────────
111 (associated_mul_left_cancel
id └────────────────────────┘
src ───────┘ └────────────────────────┘└
typ ───────┘ └────────────────────────┘└
doc ───────┘ └
txt ───────┘ └
par ───────┘ └
pid ───────┘ └
st ────────────────────────────────────
112 (by rwa [← multiset.prod_cons, ← multiset.prod_cons, multiset.cons_erase hbg]) hb
id └────────────────┘ └────────────────┘ └─────────────────┘ └─┘ └┘
src ─────────┘ ┴└─────┘└────────────────┘└──┘└────────────────┘└┘└─────────────────┘┴ ┴└┘ └
typ ─────────┘ ┴└─────┘└────────────────┘└──┘└────────────────┘└┘└─────────────────┘┴└─┘┴└┘└┘└
doc ─────────┘ ┴└─────┘ └──┘ └┘ ┴ ┴└┘ └
txt ─────────┘ ┴└─────┘ └──┘ └┘ ┴ ┴└┘ └
par ─────────┘ ┴└─────┘ └──┘ └┘ ┴ ┴└┘ └
pid ─────────┘ └──────┘ └──┘ └┘ ┴ └─┘ └
st ────────────┘└────────────────────────┘└────────────────────┘└───────────────────────┘┴└────
113 (hf p (by simp)).ne_zero))
id └┘ ┴
src ───────┘ ┴ ┴ ┴└──┘└────────────
typ ───────┘ └┘┴┴┴ ┴└──┘└────────────
doc ───────┘ ┴ ┴ ┴└──┘└────────────
txt ───────┘ ┴ ┴ ┴└──┘└────────────
par ───────┘ ┴ ┴ ┴└──┘└────────────
pid ───────┘ ┴ ┴ └─────────────────
st ────────────────┘└───┘└────────────
114 end)
src ─────────
typ ─────────
doc ─────────
txt ─────────
par ─────────
pid ───────┘└
st ───┘└─┘└─
115
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
116 end unique_factorization_domain
117
118 structure unique_irreducible_factorization (α : Type*) [integral_domain α] :=
id └───┘ └─────────────┘ ┴
src └─────────────┘
typ └───┘ └─────────────┘ ┴
119 (factors : α → multiset α)
id ┴ ┴ └──────┘ ┴
src └──────┘
typ ┴ ┴ └──────┘ ┴
doc └──────┘
120 (factors_prod : ∀{a : α}, a ≠ 0 → (factors a).prod ~ᵤ a)
id ┴ ┴ ┴ ┴ └─────┘ ┴ └──┘ └┘ ┴
src ┴ └──┘ └┘
typ ┴ ┴ ┴ ┴ └─────┘ ┴ └──┘ └┘ ┴
doc └──┘
121 (irreducible_factors : ∀{a : α}, a ≠ 0 → ∀x∈factors a, irreducible x)
id ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └─────────┘ ┴
src ┴ └─────────┘
typ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └─────────┘ ┴
doc └─────────┘
122 (unique : ∀{f g : multiset α},
id ┴ └──────┘ ┴
src ┴ └──────┘
typ ┴ └──────┘ ┴
doc └──────┘
123 (∀x∈f, irreducible x) → (∀x∈g, irreducible x) → f.prod ~ᵤ g.prod → multiset.rel associated f g)
id ┴ ┴ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴└───┘ └┘ ┴└───┘ └──────────┘ └────────┘ ┴ ┴
src └─────────┘ └─────────┘ └───┘ └┘ └───┘ └──────────┘ └────────┘
typ ┴ ┴ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴└───┘ └┘ ┴└───┘ └──────────┘ └────────┘ ┴ ┴
doc └─────────┘ └─────────┘ └───┘ └───┘ └──────────┘
124
125 namespace unique_factorization_domain
126 open unique_factorization_domain associated lattice
127 variables [integral_domain α] [unique_factorization_domain α] [decidable_eq (associates α)]
id └─────────────┘ └─────────────────────────┘ └──────────┘ └────────┘
src └─────────────┘ └─────────────────────────┘ └──────────┘ └────────┘
typ └─────────────┘ └─────────────────────────┘ └──────────┘ └────────┘
doc └─────────────────────────┘
128
129 lemma exists_mem_factors_of_dvd {a p : α} (ha0 : a ≠ 0) (hp : irreducible p) : p ∣ a →
id ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴
src ┴ └─────────┘ ┴
typ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴
doc └─────────┘
130 ∃ q ∈ factors a, p ~ᵤ q :=
id ┴ ┴ └─────┘ ┴┴ ┴ └┘ ┴
src ┴ └─────┘ ┴ └┘
typ ┴ ┴ └─────┘ ┴┴ ┴ └┘ ┴
131 λ ⟨b, hb⟩,
id ┴┴ └┘
typ ┴┴ └┘
132 have hb0 : b ≠ 0, from λ hb0, by simp * at *,
id ┴ └─┘
src ┴ └─────────┘
typ ┴ └─┘ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid ┴┴┴└──┘
st └──────────┘
133 have multiset.rel associated (p :: factors b) (factors a),
id └──────────┘ └────────┘ ┴ └┘ └─────┘ └─────┘ ┴
src └──────────┘ └────────┘ └┘ └─────┘ └─────┘
typ └──────────┘ └────────┘ ┴ └┘ └─────┘ └─────┘ ┴
doc └──────────┘ └┘
134 from unique
id └────┘
src └────┘
typ └────┘
135 (λ x hx, (multiset.mem_cons.1 hx).elim (λ h, h.symm ▸ hp)
id ┴ └┘ └───────────────┘┴ └┘ └──┘ ┴ ┴└───┘ ┴ └┘
src └───────────────┘┴ └──┘ └───┘ ┴
typ ┴ └┘ └───────────────┘┴ └┘ └──┘ ┴ ┴└───┘ ┴ └┘
136 (irreducible_factors hb0 _))
id └─────────────────┘ └─┘
src └─────────────────┘
typ └─────────────────┘ └─┘
137 (irreducible_factors ha0)
id └─────────────────┘ └─┘
src └─────────────────┘
typ └─────────────────┘ └─┘
138 (associated.symm $ calc multiset.prod (factors a) ~ᵤ a : factors_prod ha0
id └─────────────┘ └───────────┘ └─────┘ ┴ ┴ └──────────┘ └─┘
src └─────────────┘ └───────────┘ └─────┘ └──────────┘
typ └─────────────┘ └───────────┘ └─────┘ ┴ ┴ └──────────┘ └─┘
doc └───────────┘
139 ... = p * b : hb
id ┴ ┴
src ┴
typ ┴ ┴
140 ... ~ᵤ multiset.prod (p :: factors b) :
id └───────────┘ ┴ └┘ └─────┘
src └───────────┘ └┘ └─────┘
typ └───────────┘ ┴ └┘ └─────┘
doc └───────────┘ └┘
141 by rw multiset.prod_cons; exact associated_mul_mul
id └────────────────┘ └────────────────┘
src └─┘└────────────────┘ └────┘└────────────────┘└
typ └─┘└────────────────┘ └────┘└────────────────┘└
doc └─┘ └────┘ └
txt └─┘ └────┘ └
par └─┘ └────┘ └
pid ┴ ┴ └
st └────────────────────────────────────────────────
142 (associated.refl _)
id └─────────────┘
src ─────────┘ └─────────────┘└───
typ ─────────┘ └─────────────┘└───
doc ─────────┘ └───
txt ─────────┘ └───
par ─────────┘ └───
pid ─────────┘ └───
st ──────────────────────────────
143 (associated.symm (factors_prod hb0))),
id └─────────────┘ └──────────┘ └─┘
src ─────────┘ └─────────────┘┴ └──────────┘┴ └┘
typ ─────────┘ └─────────────┘┴ └──────────┘┴└─┘└┘
doc ─────────┘ ┴ ┴ └┘
txt ─────────┘ ┴ ┴ └┘
par ─────────┘ ┴ ┴ └┘
pid ─────────┘ ┴ ┴ └┘
st ─────────────────────────────────────────────┘
144 multiset.exists_mem_of_rel_of_mem this (by simp)
id └───────────────────────────────┘ └──┘
src └───────────────────────────────┘ └──┘
typ └───────────────────────────────┘ └──┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
145
146 def of_unique_irreducible_factorization {α : Type*} [integral_domain α]
id └─────────────┘ ┴
src └─────────────┘
typ └─────────────┘ ┴
147 (o : unique_irreducible_factorization α) : unique_factorization_domain α :=
id └──────────────────────────────┘ ┴ └─────────────────────────┘ ┴
src └──────────────────────────────┘ └─────────────────────────┘
typ └──────────────────────────────┘ ┴ └─────────────────────────┘ ┴
doc └─────────────────────────┘
148 by letI := classical.dec_eq α; exact
id └──────────────┘ ┴
src └──────┘└──────────────┘┴ └────┘
typ └──────┘└──────────────┘┴┴ └────┘
doc └──────┘ ┴ └────┘
txt └──────┘ ┴ └────┘
par └──────┘ ┴ └────┘
pid ┴└─┘ ┴ ┴
st └──────────────────────────────────
149 { prime_factors := λ a h p (hpa : p ∈ o.factors a),
id ┴
src └────────────────┘ └────────────┘ ┴┴┴ ┴ └──
typ └────────────────┘ └────────────┘ ┴┴┴ ┴ └──
doc └────────────────┘ └────────────┘ ┴ ┴ ┴ └──
txt └────────────────┘ └────────────┘ ┴ ┴ ┴ └──
par └────────────────┘ └────────────┘ ┴ ┴ ┴ └──
pid └────────────────┘ └────────────┘ ┴ ┴ ┴ └──
st ────────────────────────────────────────────────────
150 have hpi : irreducible p, from o.irreducible_factors h _ hpa,
id └───────────────────┘
src ───┘ └─────┘ ┴ └─────┘└───────────────────┘┴ └─┘ └─
typ ───┘ └─────┘ ┴ └─────┘└───────────────────┘┴ └─┘ └─
doc ───┘ └─────┘ ┴ └─────┘ ┴ └─┘ └─
txt ───┘ └─────┘ ┴ └─────┘ ┴ └─┘ └─
par ───┘ └─────┘ ┴ └─────┘ ┴ └─┘ └─
pid ───┘ └─────┘ ┴ └─────┘ ┴ └─┘ └─
st ──────────────────────────────────────────────────────────────────
151 ⟨hpi.ne_zero, hpi.1,
id └──────┘
src ───┘ └──────┘└┘ └───
typ ───┘ └──────┘└┘ └───
doc ───┘ └┘ └───
txt ───┘ └┘ └───
par ───┘ └┘ └───
pid ───┘ └┘ └───
st ─────────────────────────
152 λ a b ⟨x, hx⟩,
id ┴
src ─────┘ └────┘ └┘ └──
typ ─────┘ └────┘┴└┘ └──
doc ─────┘ └────┘ └┘ └──
txt ─────┘ └────┘ └┘ └──
par ─────┘ └────┘ └┘ └──
pid ─────┘ └────┘ └┘ └──
st ─────────────────────
153 if hab0 : a * b = 0
id └┘ ┴ ┴
src ─────┘└┘└──────┘ ┴┴┴ ┴┴└──
typ ─────┘└┘└──────┘ ┴┴┴ ┴┴└──
doc ─────┘ └──────┘ ┴ ┴ ┴ └──
txt ─────┘ └──────┘ ┴ ┴ ┴ └──
par ─────┘ └──────┘ ┴ ┴ ┴ └──
pid ─────┘ └──────┘ ┴ ┴ ┴ └──
st ──────────────────────────
154 then (eq_zero_or_eq_zero_of_mul_eq_zero hab0).elim
id └───────────────────────────────┘
src ──────────┘ └───────────────────────────────┘┴ └──────
typ ──────────┘ └───────────────────────────────┘┴ └──────
doc ──────────┘ ┴ └──────
txt ──────────┘ ┴ └──────
par ──────────┘ ┴ └──────
pid ──────────┘ ┴ └──────
st ─────────────────────────────────────────────────────────
155 (λ ha0, by simp [ha0])
id └─┘
src ───────┘ └────┘ ┴└────┘ ┴└─
typ ───────┘ └────┘ ┴└────┘└─┘┴└─
doc ───────┘ └────┘ ┴└────┘ ┴└─
txt ───────┘ └────┘ ┴└────┘ ┴└─
par ───────┘ └────┘ ┴└────┘ ┴└─
pid ───────┘ └────┘ └─────┘ └──
st ─────────────────┘└─────────┘└─
156 (λ hb0, by simp [hb0])
id └─┘
src ───────┘ └────┘ ┴└────┘ ┴└─
typ ───────┘ └────┘ ┴└────┘└─┘┴└─
doc ───────┘ └────┘ ┴└────┘ ┴└─
txt ───────┘ └────┘ ┴└────┘ ┴└─
par ───────┘ └────┘ ┴└────┘ ┴└─
pid ───────┘ └────┘ └─────┘ └──
st ─────────────────┘└─────────┘└─
157 else
src ───────────
typ ───────────
doc ───────────
txt ───────────
par ───────────
pid ───────────
st ───────────
158 have hx0 : x ≠ 0, from λ hx0, by simp * at *,
id └──┘ ┴
src ───────┘ └─────┘ ┴┴└───────┘ └────┘ ┴└─────────┘└─
typ ───────┘└──┘└─────┘ ┴┴└───────┘ └────┘ ┴└─────────┘└─
doc ───────┘ └─────┘ ┴ └───────┘ └────┘ ┴└─────────┘└─
txt ───────┘ └─────┘ ┴ └───────┘ └────┘ ┴└─────────┘└─
par ───────┘ └─────┘ ┴ └───────┘ └────┘ ┴└─────────┘└─
pid ───────┘ └─────┘ ┴ └───────┘ └────┘ └─────────────
st ───────────────────────────────────────┘└──────────┘└─
159 have ha0 : a ≠ 0, from ne_zero_of_mul_ne_zero_right hab0,
id └──────────────────────────┘
src ───────┘ └─────┘ ┴ └───────┘└──────────────────────────┘┴ └─
typ ───────┘ └─────┘ ┴ └───────┘└──────────────────────────┘┴ └─
doc ───────┘ └─────┘ ┴ └───────┘ ┴ └─
txt ───────┘ └─────┘ ┴ └───────┘ ┴ └─
par ───────┘ └─────┘ ┴ └───────┘ ┴ └─
pid ───────┘ └─────┘ ┴ └───────┘ ┴ └─
st ──────────────────────────────────────────────────────────────────
160 have hb0 : b ≠ 0, from ne_zero_of_mul_ne_zero_left hab0,
id └─────────────────────────┘
src ───────┘ └─────┘ ┴ └───────┘└─────────────────────────┘┴ └─
typ ───────┘ └─────┘ ┴ └───────┘└─────────────────────────┘┴ └─
doc ───────┘ └─────┘ ┴ └───────┘ ┴ └─
txt ───────┘ └─────┘ ┴ └───────┘ ┴ └─
par ───────┘ └─────┘ ┴ └───────┘ ┴ └─
pid ───────┘ └─────┘ ┴ └───────┘ ┴ └─
st ─────────────────────────────────────────────────────────────────
161 have multiset.rel associated (p :: o.factors x) (o.factors a + o.factors b),
id └────────┘ └┘ ┴
src ───────┘ └────────────┘└────────┘└┘ ┴└┘┴ ┴ └┘ ┴ ┴┴┴ ┴ └──
typ ───────┘ └────────────┘└────────┘└┘ ┴└┘┴ ┴ └┘ ┴ ┴┴┴ ┴ └──
doc ───────┘ └────────────┘ └┘ ┴└┘┴ ┴ └┘ ┴ ┴ ┴ ┴ └──
txt ───────┘ └────────────┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──
par ───────┘ └────────────┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──
pid ───────┘ └────────────┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──
st ──────────────────────────────────────────────────────────────────────────────────────
162 from o.unique
id └──────┘
src ──────────────┘└──────┘└
typ ──────────────┘└──────┘└
doc ──────────────┘ └
txt ──────────────┘ └
par ──────────────┘ └
pid ──────────────┘ └
st ────────────────────────
163 (λ i hi, (multiset.mem_cons.1 hi).elim
id └───────────────┘
src ───────────┘ └─────┘ └───────────────┘└─┘ └──────
typ ───────────┘ └─────┘ └───────────────┘└─┘ └──────
doc ───────────┘ └─────┘ └─┘ └──────
txt ───────────┘ └─────┘ └─┘ └──────
par ───────────┘ └─────┘ └─┘ └──────
pid ───────────┘ └─────┘ └─┘ └──────
st ───────────────────────────────────────────────────
164 (λ hip, hip.symm ▸ hpi)
id └───┘ ┴
src ─────────────┘ └────┘ └───┘┴┴┴ └─
typ ─────────────┘ └────┘ └───┘┴┴┴ └─
doc ─────────────┘ └────┘ ┴ ┴ └─
txt ─────────────┘ └────┘ ┴ ┴ └─
par ─────────────┘ └────┘ ┴ ┴ └─
pid ─────────────┘ └────┘ ┴ ┴ └─
st ──────────────────────────────────────
165 (o.irreducible_factors hx0 _))
src ─────────────┘ ┴ └────
typ ─────────────┘ ┴ └────
doc ─────────────┘ ┴ └────
txt ─────────────┘ ┴ └────
par ─────────────┘ ┴ └────
pid ─────────────┘ ┴ └────
st ─────────────────────────────────────────────
166 (show ∀ x ∈ o.factors a + o.factors b, irreducible x,
id └─────────┘
src ───────────┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴└─────────┘┴ └─
typ ───────────┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴└─────────┘┴ └─
doc ───────────┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴└─────────┘┴ └─
txt ───────────┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
par ───────────┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
pid ───────────┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
st ──────────────────────────────────────────────────────────────────
167 from λ x hx, (multiset.mem_add.1 hx).elim
id └──────────────┘
src ──────────────────┘ └─────┘ └──────────────┘└─┘ └──────
typ ──────────────────┘ └─────┘ └──────────────┘└─┘ └──────
doc ──────────────────┘ └─────┘ └─┘ └──────
txt ──────────────────┘ └─────┘ └─┘ └──────
par ──────────────────┘ └─────┘ └─┘ └──────
pid ──────────────────┘ └─────┘ └─┘ └──────
st ────────────────────────────────────────────────────────
168 (o.irreducible_factors (ne_zero_of_mul_ne_zero_right hab0) _)
src ───────────────┘ ┴ ┴ └────
typ ───────────────┘ ┴ ┴ └────
doc ───────────────┘ ┴ ┴ └────
txt ───────────────┘ ┴ ┴ └────
par ───────────────┘ ┴ ┴ └────
pid ───────────────┘ ┴ ┴ └────
st ──────────────────────────────────────────────────────────────────────────────
169 (o.irreducible_factors (ne_zero_of_mul_ne_zero_left hab0) _)) $
src ───────────────┘ ┴ ┴ └────┘ └
typ ───────────────┘ ┴ ┴ └────┘ └
doc ───────────────┘ ┴ ┴ └────┘ └
txt ───────────────┘ ┴ ┴ └────┘ └
par ───────────────┘ ┴ ┴ └────┘ └
pid ───────────────┘ ┴ ┴ └────┘ └
st ────────────────────────────────────────────────────────────────────────────────
170 calc multiset.prod (p :: o.factors x)
id └───────────┘
src ─────────────┘ ┴└───────────┘┴ ┴ ┴ ┴ └─
typ ─────────────┘ ┴└───────────┘┴ ┴ ┴ ┴ └─
doc ─────────────┘ ┴└───────────┘┴ ┴ ┴ ┴ └─
txt ─────────────┘ ┴ ┴ ┴ ┴ ┴ └─
par ─────────────┘ ┴ ┴ ┴ ┴ ┴ └─
pid ─────────────┘ ┴ ┴ ┴ ┴ ┴ └─
st ────────────────────────────────────────────────────
171 ~ᵤ a * b : by rw [hx, multiset.prod_cons];
id └┘ └────────────────┘
src ─────────────────┘ ┴ ┴ ┴ └─┘ ┴└──┘ └┘└────────────────┘┴└─
typ ─────────────────┘ ┴ ┴ ┴ └─┘ ┴└──┘└┘└┘└────────────────┘┴└─
doc ─────────────────┘ ┴ ┴ ┴ └─┘ ┴└──┘ └┘ ┴└─
txt ─────────────────┘ ┴ ┴ ┴ └─┘ ┴└──┘ └┘ ┴└─
par ─────────────────┘ ┴ ┴ ┴ └─┘ ┴└──┘ └┘ ┴└─
pid ─────────────────┘ ┴ ┴ ┴ └─┘ └───┘ └┘ └──
st ──────────────────────────────┘└─────┘└──────────────────┘┴└─
172 exact associated_mul_mul (by refl)
id └────────────────┘
src ─────────────────────────┘└────────────────┘┴ ┴└──┘└─
typ ─────────────────────────┘└────────────────┘┴ ┴└──┘└─
doc ─────────────────────────┘ ┴ ┴└──┘└─
txt ─────────────────────────┘ ┴ ┴└──┘└─
par ─────────────────────────┘ ┴ ┴└──┘└─
pid ─────────────────────────┘ ┴ └──────
st ───────────────────────────────────────────────┘└───┘└─
173 (o.factors_prod hx0)
id └────────────┘ └─┘
src ─────────────────────┘ └────────────┘┴ └─
typ ─────────────────────┘ └────────────┘┴└─┘└─
doc ─────────────────────┘ ┴ └─
txt ─────────────────────┘ ┴ └─
par ─────────────────────┘ ┴ └─
pid ─────────────────────┘ ┴ └─
st ───────────────────────────────────────────
174 ... ~ᵤ (o.factors a).prod * (o.factors b).prod :
id └───────┘
src ─────────────────┘ ┴ ┴ └─────┘ ┴ └───────┘┴ └────────
typ ─────────────────┘ ┴ ┴ └─────┘ ┴ └───────┘┴ └────────
doc ─────────────────┘ ┴ ┴ └─────┘ ┴ ┴ └────────
txt ─────────────────┘ ┴ ┴ └─────┘ ┴ ┴ └────────
par ─────────────────┘ ┴ ┴ └─────┘ ┴ ┴ └────────
pid ─────────────────┘ ┴ ┴ └─────┘ ┴ ┴ └────────
st ─────────────┘└────────────────────────────────────────────────
175 associated_mul_mul
id └────────────────┘
src ───────────────┘└────────────────┘└
typ ───────────────┘└────────────────┘└
doc ───────────────┘ └
txt ───────────────┘ └
par ───────────────┘ └
pid ───────────────┘ └
st ───────────────────────────────────
176 (o.factors_prod ha0).symm
src ─────────────────┘ ┴ └──────
typ ─────────────────┘ ┴ └──────
doc ─────────────────┘ ┴ └──────
txt ─────────────────┘ ┴ └──────
par ─────────────────┘ ┴ └──────
pid ─────────────────┘ ┴ └──────
st ────────────────────────────────────────────
177 (o.factors_prod hb0).symm
id └────────────┘
src ─────────────────┘ └────────────┘┴ └──────
typ ─────────────────┘ └────────────┘┴ └──────
doc ─────────────────┘ ┴ └──────
txt ─────────────────┘ ┴ └──────
par ─────────────────┘ ┴ └──────
pid ─────────────────┘ ┴ └──────
st ────────────────────────────────────────────
178 ... = _ : by rw multiset.prod_add,
id └───────────────┘
src ─────────────────┘ └───┘ ┴└─┘└───────────────┘└─
typ ─────────────────┘ └───┘ ┴└─┘└───────────────┘└─
doc ─────────────────┘ └───┘ ┴└─┘ └─
txt ─────────────────┘ └───┘ ┴└─┘ └─
par ─────────────────┘ └───┘ ┴└─┘ └─
pid ─────────────────┘ └───┘ └──┘ └─
st ─────────────────────────┘└───────────────────┘└─
179 let ⟨q, hqf, hq⟩ := multiset.exists_mem_of_rel_of_mem this
id └─┘ └┘ └───────────────────────────────┘
src ───────┘ ┴ └┘ └┘ └───┘└───────────────────────────────┘┴ └
typ ───────┘ ┴ └┘└─┘└┘└┘└───┘└───────────────────────────────┘┴ └
doc ───────┘ ┴ └┘ └┘ └───┘ ┴ └
txt ───────┘ ┴ └┘ └┘ └───┘ ┴ └
par ───────┘ ┴ └┘ └┘ └───┘ ┴ └
pid ───────┘ ┴ └┘ └┘ └───┘ ┴ └
st ───────────────────────────────────────────────────────────────────
180 (multiset.mem_cons_self p _) in
id └────────────────────┘
src ─────────┘ └────────────────────┘┴ └──────
typ ─────────┘ └────────────────────┘┴ └──────
doc ─────────┘ ┴ └──────
txt ─────────┘ ┴ └──────
par ─────────┘ ┴ └──────
pid ─────────┘ ┴ └──────
st ──────────────────────────────────────────
181 (multiset.mem_add.1 hqf).elim
src ───────┘ └─┘ └──────
typ ───────┘ └─┘ └──────
doc ───────┘ └─┘ └──────
txt ───────┘ └─┘ └──────
par ───────┘ └─┘ └──────
pid ───────┘ └─┘ └──────
st ──────────────────────────────────────
182 (λ hqa, or.inl $ (dvd_iff_dvd_of_rel_left hq).2 $
id └────┘
src ─────────┘ └────┘└────┘┴ ┴ ┴ └──┘ └
typ ─────────┘ └────┘└────┘┴ ┴ ┴ └──┘ └
doc ─────────┘ └────┘ ┴ ┴ ┴ └──┘ └
txt ─────────┘ └────┘ ┴ ┴ ┴ └──┘ └
par ─────────┘ └────┘ ┴ ┴ ┴ └──┘ └
pid ─────────┘ └────┘ ┴ ┴ ┴ └──┘ └
st ────────────────────────────────────────────────────────────
183 (dvd_iff_dvd_of_rel_right (o.factors_prod ha0)).1
src ───────────┘ ┴ ┴ └────
typ ───────────┘ ┴ ┴ └────
doc ───────────┘ ┴ ┴ └────
txt ───────────┘ ┴ ┴ └────
par ───────────┘ ┴ ┴ └────
pid ───────────┘ ┴ ┴ └────
st ──────────────────────────────────────────────────────────────
184 (multiset.dvd_prod hqa))
src ─────────────┘ ┴ └──
typ ─────────────┘ ┴ └──
doc ─────────────┘ ┴ └──
txt ─────────────┘ ┴ └──
par ─────────────┘ ┴ └──
pid ─────────────┘ ┴ └──
st ───────────────────────────────────────
185 (λ hqb, or.inr $ (dvd_iff_dvd_of_rel_left hq).2 $
id └────┘ └─────────────────────┘
src ─────────┘ └────┘└────┘┴ ┴ └─────────────────────┘┴ └──┘ └
typ ─────────┘ └────┘└────┘┴ ┴ └─────────────────────┘┴ └──┘ └
doc ─────────┘ └────┘ ┴ ┴ ┴ └──┘ └
txt ─────────┘ └────┘ ┴ ┴ ┴ └──┘ └
par ─────────┘ └────┘ ┴ ┴ ┴ └──┘ └
pid ─────────┘ └────┘ ┴ ┴ ┴ └──┘ └
st ────────────────────────────────────────────────────────────
186 (dvd_iff_dvd_of_rel_right (o.factors_prod hb0)).1
id └──────────────────────┘
src ───────────┘ └──────────────────────┘┴ ┴ └────
typ ───────────┘ └──────────────────────┘┴ ┴ └────
doc ───────────┘ ┴ ┴ └────
txt ───────────┘ ┴ ┴ └────
par ───────────┘ ┴ ┴ └────
pid ───────────┘ ┴ ┴ └────
st ──────────────────────────────────────────────────────────────
187 (multiset.dvd_prod hqb))⟩,
id └───────────────┘
src ─────────────┘ └───────────────┘┴ └────
typ ─────────────┘ └───────────────┘┴ └────
doc ─────────────┘ ┴ └────
txt ─────────────┘ ┴ └────
par ─────────────┘ ┴ └────
pid ─────────────┘ ┴ └────
st ─────────────────────────────────────────
188 ..o }
id ┴
src ───┘ └──
typ ───┘┴└──
doc ───┘ └──
txt ───┘ └──
par ───┘ └──
pid ───┘ └┘└
st ────────
189
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
190 end unique_factorization_domain
191
192 namespace associates
193 open unique_factorization_domain associated lattice
194 variables [integral_domain α] [unique_factorization_domain α] [decidable_eq (associates α)]
id └─────────────┘ └─────────────────────────┘ └──────────┘ └────────┘
src └─────────────┘ └─────────────────────────┘ └──────────┘ └────────┘
typ └─────────────┘ └─────────────────────────┘ └──────────┘ └────────┘
doc └─────────────────────────┘
195
196 /-- `factor_set α` representation elements of unique factorization domain as multisets.
197
198 `multiset α` produced by `factors` are only unique up to associated elements, while the multisets in
199 `factor_set α` are unqiue by equality and restricted to irreducible elements. This gives us a
200 representation of each element as a unique multisets (or the added ⊤ for 0), which has a complete
201 lattice struture. Infimum is the greatest common divisor and supremum is the least common multiple.
202 -/
203 @[reducible] def {u} factor_set (α : Type u) [integral_domain α] [unique_factorization_domain α] :
id └─────────────┘ ┴ └─────────────────────────┘ ┴
src └─────────────┘ └─────────────────────────┘
typ └─────────────┘ ┴ └─────────────────────────┘ ┴
doc └───────┘ └─────────────────────────┘
204 Type u :=
205 with_top (multiset { a : associates α // irreducible a })
id └──────┘ └──────┘ ┴ └────────┘ ┴ └─────────┘ ┴
src └──────┘ └──────┘ ┴ └────────┘ └─────────┘
typ └──────┘ └──────┘ ┴ └────────┘ ┴ └─────────┘ ┴
doc └──────┘ └─────────┘
206
207 local attribute [instance] associated.setoid
id └───────────────┘
src └───────────────┘
typ └───────────────┘
208
209 theorem unique' {p q : multiset (associates α)} :
id └──────┘ └────────┘ ┴
src └──────┘ └────────┘
typ └──────┘ └────────┘ ┴
doc └──────┘
210 (∀a∈p, irreducible a) → (∀a∈q, irreducible a) → p.prod = q.prod → p = q :=
id ┴ ┴ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴└───┘ ┴ ┴└───┘ ┴ ┴ ┴
src └─────────┘ └─────────┘ └───┘ ┴ └───┘ ┴
typ ┴ ┴ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴└───┘ ┴ ┴└───┘ ┴ ┴ ┴
doc └─────────┘ └─────────┘ └───┘ └───┘
211 begin
st └─────
212 apply multiset.induction_on_multiset_quot p,
id └─────────────────────────────────┘ ┴
src └────┘└─────────────────────────────────┘┴
typ └────┘└─────────────────────────────────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────────────────────────────┘└─
213 apply multiset.induction_on_multiset_quot q,
id └─────────────────────────────────┘ ┴
src └────┘└─────────────────────────────────┘┴
typ └────┘└─────────────────────────────────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────────────────────────────┘└─
214 assume s t hs ht eq,
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
txt └─────────────────┘
par └─────────────────┘
pid └─────────────────┘
st ────────────────────┘└─
215 refine multiset.map_mk_eq_map_mk_of_rel (unique_factorization_domain.unique _ _ _),
id └──────────────────────────────┘ └────────────────────────────────┘
src └─────┘└──────────────────────────────┘┴ └────────────────────────────────┘└─────┘
typ └─────┘└──────────────────────────────┘┴ └────────────────────────────────┘└─────┘
doc └─────┘ ┴ └─────┘
txt └─────┘ ┴ └─────┘
par └─────┘ ┴ └─────┘
pid ┴ ┴ └─────┘
st ───────────────────────────────────────────────────────────────────────────────────┘└─
216 { exact assume a ha, ((irreducible_mk_iff _).1 $ hs _ $ multiset.mem_map_of_mem _ ha) },
id └────────────────┘ └┘ └─────────────────────┘
src └────┘ └─────┘ └────────────────┘└────┘ ┴ └─┘ ┴└─────────────────────┘└─┘ └┘
typ └────┘ └─────┘ └────────────────┘└────┘ ┴└┘└─┘ ┴└─────────────────────┘└─┘ └┘
doc └────┘ └─────┘ └────┘ ┴ └─┘ ┴ └─┘ └┘
txt └────┘ └─────┘ └────┘ ┴ └─┘ ┴ └─┘ └┘
par └────┘ └─────┘ └────┘ ┴ └─┘ ┴ └─┘ └┘
pid ┴ └─────┘ └────┘ ┴ └─┘ ┴ └─┘ ┴┴
st ───┘└──────────────────────────────────────────────────────────────────────────────────┘└┘└
217 { exact assume a ha, ((irreducible_mk_iff _).1 $ ht _ $ multiset.mem_map_of_mem _ ha) },
id └────────────────┘ └┘ └─────────────────────┘
src └────┘ └─────┘ └────────────────┘└────┘ ┴ └─┘ ┴└─────────────────────┘└─┘ └┘
typ └────┘ └─────┘ └────────────────┘└────┘ ┴└┘└─┘ ┴└─────────────────────┘└─┘ └┘
doc └────┘ └─────┘ └────┘ ┴ └─┘ ┴ └─┘ └┘
txt └────┘ └─────┘ └────┘ ┴ └─┘ ┴ └─┘ └┘
par └────┘ └─────┘ └────┘ ┴ └─┘ ┴ └─┘ └┘
pid ┴ └─────┘ └────┘ ┴ └─┘ ┴ └─┘ ┴┴
st ───┘└──────────────────────────────────────────────────────────────────────────────────┘└┘└
218 simpa [quot_mk_eq_mk, prod_mk, mk_eq_mk_iff_associated] using eq
id └───────────┘ └─────┘ └─────────────────────┘ └┘
src └─────┘└───────────┘└┘└─────┘└┘└─────────────────────┘└──────┘└┘┴
typ └─────┘└───────────┘└┘└─────┘└┘└─────────────────────┘└──────┘└┘┴
doc └─────┘ └┘ └┘ └──────┘ ┴
txt └─────┘ └┘ └┘ └──────┘ ┴
par └─────┘ └┘ └┘ └──────┘ ┴
pid ┴┴ └┘ └┘ ┴┴└────┘ ┴
st ──────────────────────────────────────────────────────────────────┘
219 end
st └─┘
220
221 private theorem forall_map_mk_factors_irreducible (x : α) (hx : x ≠ 0) :
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
222 ∀(a : associates α), a ∈ multiset.map associates.mk (factors x) → irreducible a :=
id └────────┘ ┴ ┴ ┴ └──────────┘ └───────────┘ └─────┘ ┴ └─────────┘ ┴
src └────────┘ ┴ └──────────┘ └───────────┘ └─────┘ └─────────┘
typ └────────┘ ┴ ┴ ┴ └──────────┘ └───────────┘ └─────┘ ┴ └─────────┘ ┴
doc └──────────┘ └─────────┘
223 begin
st └─────
224 assume a ha,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────┘└─
225 rcases multiset.mem_map.1 ha with ⟨c, hc, rfl⟩,
id └──────────────┘ └┘
src └─────┘└──────────────┘└─┘ └────────────────┘
typ └─────┘└──────────────┘└─┘└┘└────────────────┘
doc └─────┘ └─┘ └────────────────┘
txt └─────┘ └─┘ └────────────────┘
par └─────┘ └─┘ └────────────────┘
pid ┴ └─┘ └────────────────┘
st ───────────────────────────────────────────────┘└─
226 exact (irreducible_mk_iff c).2 (irreducible_factors hx _ hc)
id └────────────────┘ ┴ └─────────────────┘ └┘ └┘
src └────┘ └────────────────┘┴ └──┘ └─────────────────┘┴ └─┘ └┘
typ └────┘ └────────────────┘┴┴└──┘ └─────────────────┘┴└┘└─┘└┘└┘
doc └────┘ ┴ └──┘ ┴ └─┘ └┘
txt └────┘ ┴ └──┘ ┴ └─┘ └┘
par └────┘ ┴ └──┘ ┴ └─┘ └┘
pid ┴ ┴ └──┘ ┴ └─┘ ┴┴
st ──────────────────────────────────────────────────────────────┘
227 end
st └─┘
228
229 theorem prod_le_prod_iff_le {p q : multiset (associates α)}
id └──────┘ └────────┘ ┴
src └──────┘ └────────┘
typ └──────┘ └────────┘ ┴
doc └──────┘
230 (hp : ∀a∈p, irreducible a) (hq : ∀a∈q, irreducible a) :
id ┴ ┴ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ ┴ ┴ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
231 p.prod ≤ q.prod ↔ p ≤ q :=
id ┴└───┘ ┴ ┴└───┘ ┴ ┴ ┴ ┴
src └───┘ ┴ └───┘ ┴ ┴
typ ┴└───┘ ┴ ┴└───┘ ┴ ┴ ┴ ┴
doc └───┘ └───┘
232 iff.intro
id └───────┘
src └───────┘
typ └───────┘
233 begin
st └─────
234 rintros ⟨⟨c⟩, eq⟩,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └────────┘
st ────────────────────┘└─
235 have : c ≠ 0, from (mt mk_eq_zero_iff_eq_zero.2 $
id ┴ ┴ └┘ └────────────────────┘
src └─────┘ ┴┴└┘ └───┘ └┘┴└────────────────────┘└─┘ └
typ └─────┘┴┴┴└┘ └───┘ └┘┴└────────────────────┘└─┘ └
doc └─────┘ ┴ └┘ └───┘ ┴ └─┘ └
txt └─────┘ ┴ └┘ └───┘ ┴ └─┘ └
par └─────┘ ┴ └┘ └───┘ ┴ └─┘ └
pid └───┘└┘ ┴ ┴┴ └───┘ ┴ └─┘ └
st ───────────────┘└─────────────────────────────────────
236 assume (hc : quot.mk setoid.r c = 0),
id └─────┘ └──────┘ ┴ ┴
src ─────┘ └─────┘ ┴└──────┘┴ ┴┴└────
typ ─────┘ └─────┘└─────┘┴└──────┘┴┴┴┴└────
doc ─────┘ └─────┘ ┴ ┴ ┴ └────
txt ─────┘ └─────┘ ┴ ┴ ┴ └────
par ─────┘ └─────┘ ┴ ┴ ┴ └────
pid ─────┘ └─────┘ ┴ ┴ ┴ └────
st ────────────────────────────────────────────
237 have (0 : associates α) ∈ q, from prod_eq_zero_iff.1 $ eq ▸ hc.symm ▸ mul_zero _,
id └────────┘ ┴ ┴ ┴ └──────────────┘ └┘ ┴ └───┘ └──────┘
src ─────┘ ┴ └──┘└────────┘┴ └┘┴┴ └─────┘└──────────────┘└─┘ ┴└┘┴┴┴ └───┘┴ ┴└──────┘└───
typ ─────┘ ┴ └──┘└────────┘┴┴└┘┴┴┴└─────┘└──────────────┘└─┘ ┴└┘┴┴┴ └───┘┴ ┴└──────┘└───
doc ─────┘ ┴ └──┘ ┴ └┘ ┴ └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ └───
txt ─────┘ ┴ └──┘ ┴ └┘ ┴ └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ └───
par ─────┘ ┴ └──┘ ┴ └┘ ┴ └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ └───
pid ─────┘ ┴ └──┘ ┴ └┘ ┴ └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ └───
st ────────────────────────────────────────────────────────────────────────────────────────
238 not_irreducible_zero ((irreducible_mk_iff 0).1 $ hq _ this)),
id └──────────────────┘ └────────────────┘ └┘
src ─────┘└──────────────────┘┴ └────────────────┘└────┘ ┴ └─┘ └┘
typ ─────┘└──────────────────┘┴ └────────────────┘└────┘ ┴└┘└─┘ └┘
doc ─────┘ ┴ └────┘ ┴ └─┘ └┘
txt ─────┘ ┴ └────┘ ┴ └─┘ └┘
par ─────┘ ┴ └────┘ ┴ └─┘ └┘
pid ─────┘ ┴ └────┘ ┴ └─┘ └┘
st ─────────────────────────────────────────────────────────────────┘└─
239 have : associates.mk (factors c).prod = quot.mk setoid.r c,
id └───────────┘ └─────┘ └─────┘ └──────┘ ┴
src └─────┘└───────────┘┴ └─────┘┴ └─────┘ ┴ ┴└──────┘┴
typ └─────┘└───────────┘┴ └─────┘┴ └─────┘ ┴└─────┘┴└──────┘┴┴
doc └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴
txt └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴
par └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ └─────┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────┘└─
240 from mk_eq_mk_iff_associated.2 (factors_prod this),
id └─────────────────────┘ └──────────┘ └──┘
src └───┘└─────────────────────┘└─┘ └──────────┘┴ ┴
typ └───┘└─────────────────────┘└─┘ └──────────┘┴└──┘┴
doc └───┘ └─┘ ┴ ┴
txt └───┘ └─┘ ┴ ┴
par └───┘ └─┘ ┴ ┴
pid └───┘ └─┘ ┴ ┴
st ───────────────────────────────────────────────────────┘└─
241
st ─
242 refine le_iff_exists_add.2 ⟨(factors c).map associates.mk, unique' hq _ _⟩,
id └───────────────┘ └─────┘ ┴ └───────────┘ └─────┘ └┘
src └─────┘└───────────────┘└─┘ └─────┘┴ └────┘└───────────┘└┘└─────┘┴ └───┘
typ └─────┘└───────────────┘└─┘ └─────┘┴┴└────┘└───────────┘└┘└─────┘┴└┘└───┘
doc └─────┘ └─┘ ┴ └────┘ └┘ ┴ └───┘
txt └─────┘ └─┘ ┴ └────┘ └┘ ┴ └───┘
par └─────┘ └─┘ ┴ └────┘ └┘ ┴ └───┘
pid ┴ └─┘ ┴ └────┘ └┘ ┴ └───┘
st ─────────────────────────────────────────────────────────────────────────────┘└─
243 { assume x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ─────┘└─────────┘└─
244 rcases multiset.mem_add.1 hx with h | h,
id └──────────────┘ └┘
src └─────┘└──────────────┘└─┘ └─────────┘
typ └─────┘└──────────────┘└─┘└┘└─────────┘
doc └─────┘ └─┘ └─────────┘
txt └─────┘ └─┘ └─────────┘
par └─────┘ └─┘ └─────────┘
pid ┴ └─┘ └─────────┘
st ────────────────────────────────────────────┘└─
245 exact hp x h,
id └┘ ┴ ┴
src └────┘ ┴ ┴
typ └────┘└┘┴┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────────────────┘└─
246 exact forall_map_mk_factors_irreducible c ‹c ≠ 0› _ h },
id └───────────────────────────────┘ ┴┴ ┴ ┴
src └────┘└───────────────────────────────┘┴ ┴┴ ┴ └┘┴└─┘ ┴
typ └────┘└───────────────────────────────┘┴ ┴┴┴┴ └┘┴└─┘┴┴
doc └────┘ ┴ ┴┴ ┴ └┘┴└─┘ ┴
txt └────┘ ┴ ┴ ┴ └┘ └─┘ ┴
par └────┘ ┴ ┴ ┴ └┘ └─┘ ┴
pid ┴ ┴ ┴ ┴ └┘ └─┘ ┴
st ───────────────────────────────────────────────────────────┘└┘└
247 { simp [multiset.prod_add, prod_mk, *] at * }
id └───────────────┘ └─────┘
src └────┘└───────────────┘└┘└─────┘└────────┘
typ └────┘└───────────────┘└┘└─────┘└────────┘
doc └────┘ └┘ └────────┘
txt └────┘ └┘ └────────┘
par └────┘ └┘ └────────┘
pid ┴┴ └┘ └──┘┴└──┘┴
st ───────────────────────────────────────────────┘└─
248 end
st ────┘
249 prod_le_prod
id └──────────┘
src └──────────┘
typ └──────────┘
250
251 @[simp] theorem factor_set.coe_add {a b : multiset { a : associates α // irreducible a }} :
id └──────┘ ┴ └────────┘ ┴ └─────────┘ ┴
src └──────┘ ┴ └────────┘ └─────────┘
typ └──────┘ ┴ └────────┘ ┴ └─────────┘ ┴
doc └──┘ └──────┘ └─────────┘
252 (↑a + ↑b : factor_set α) = ↑(a + b) :=
id ┴┴ ┴ ┴┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └────────┘ ┴ ┴ ┴
typ ┴┴ ┴ ┴┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘
253 with_top.coe_add
id └──────────────┘
src └──────────────┘
typ └──────────────┘
254
255 lemma factor_set.sup_add_inf_eq_add : ∀(a b : factor_set α), a ⊔ b + a ⊓ b = a + b
id ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘
256 | none b := show ⊤ ⊔ b + ⊤ ⊓ b = ⊤ + b, by simp
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
257 | a none := show a ⊔ ⊤ + a ⊓ ⊤ = a + ⊤, by simp
id ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘
typ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
258 | (some a) (some b) := show (a : factor_set α) ⊔ b + a ⊓ b = a + b, from
id ┴ └──┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ └────────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └──┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘
259 begin
st └─────
260 rw [← with_top.coe_sup, ← with_top.coe_inf, ← with_top.coe_add, ← with_top.coe_add,
id └──────────────┘ └──────────────┘ └──────────────┘ └──────────────┘
src └────┘└──────────────┘└──┘└──────────────┘└──┘└──────────────┘└──┘└──────────────┘└─
typ └────┘└──────────────┘└──┘└──────────────┘└──┘└──────────────┘└──┘└──────────────┘└─
doc └────┘ └──┘ └──┘ └──┘ └─
txt └────┘ └──┘ └──┘ └──┘ └─
par └────┘ └──┘ └──┘ └──┘ └─
pid └──┘ └──┘ └──┘ └──┘ └─
st ─────────────────────────┘└──────────────────┘└──────────────────┘└──────────────────┘└─
261 with_top.coe_eq_coe],
id └─────────────────┘
src ─────┘└─────────────────┘┴
typ ─────┘└─────────────────┘┴
doc ─────┘ ┴
txt ─────┘ ┴
par ─────┘ ┴
pid ─────┘ ┴
st ────────────────────────┘└──
262 exact multiset.union_add_inter _ _
id └──────────────────────┘
src └────┘└──────────────────────┘└────
typ └────┘└──────────────────────┘└────
doc └────┘ └────
txt └────┘ └────
par └────┘ └────
pid ┴ └──┘└
st ───────────────────────────────────────
263 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
264
265 def factors' (a : α) (ha : a ≠ 0) : multiset { a : associates α // irreducible a } :=
id ┴ ┴ ┴ └──────┘ ┴ └────────┘ ┴ └─────────┘ ┴
src ┴ └──────┘ ┴ └────────┘ └─────────┘
typ ┴ ┴ ┴ └──────┘ ┴ └────────┘ ┴ └─────────┘ ┴
doc └──────┘ └─────────┘
266 (factors a).pmap (λa ha, ⟨associates.mk a, (irreducible_mk_iff _).2 ha⟩)
id └─────┘ ┴ └──┘ ┴ └┘ └───────────┘ ┴ └────────────────┘ ┴ └┘
src └─────┘ └──┘ └───────────┘ └────────────────┘ ┴
typ └─────┘ ┴ └──┘ ┴ └┘ └───────────┘ ┴ └────────────────┘ ┴ └┘
doc └──┘
267 (irreducible_factors $ ha)
id └─────────────────┘ └┘
src └─────────────────┘
typ └─────────────────┘ └┘
268
269 @[simp] theorem map_subtype_val_factors' {a : α} (ha : a ≠ 0) :
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
doc └──┘
270 (factors' a ha).map subtype.val = (factors a).map associates.mk :=
id └──────┘ ┴ └┘ └─┘ └─────────┘ ┴ └─────┘ ┴ └─┘ └───────────┘
src └──────┘ └─┘ └─────────┘ ┴ └─────┘ └─┘ └───────────┘
typ └──────┘ ┴ └┘ └─┘ └─────────┘ ┴ └─────┘ ┴ └─┘ └───────────┘
doc └─┘ └─┘
271 by simp [factors', multiset.map_pmap, multiset.pmap_eq_map]
id └──────┘ └───────────────┘ └──────────────────┘
src └────┘└──────┘└┘└───────────────┘└┘└──────────────────┘└─
typ └────┘└──────┘└┘└───────────────┘└┘└──────────────────┘└─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st └─────────────────────────────────────────────────────────
272
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
273 theorem factors'_cong {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) (h : a ~ᵤ b) :
id ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
274 factors' a ha = factors' b hb :=
id └──────┘ ┴ └┘ ┴ └──────┘ ┴ └┘
src └──────┘ ┴ └──────┘
typ └──────┘ ┴ └┘ ┴ └──────┘ ┴ └┘
275 have multiset.rel associated (factors a) (factors b), from
id └──────────┘ └────────┘ └─────┘ ┴ └─────┘ ┴
src └──────────┘ └────────┘ └─────┘ └─────┘
typ └──────────┘ └────────┘ └─────┘ ┴ └─────┘ ┴
doc └──────────┘
276 unique (irreducible_factors ha) (irreducible_factors hb)
id └────┘ └─────────────────┘ └┘ └─────────────────┘ └┘
src └────┘ └─────────────────┘ └─────────────────┘
typ └────┘ └─────────────────┘ └┘ └─────────────────┘ └┘
277 ((factors_prod ha).trans $ h.trans $ (factors_prod hb).symm),
id └──────────┘ └┘ └───┘ ┴└────┘ └──────────┘ └┘ └──┘
src └──────────┘ └───┘ └────┘ └──────────┘ └──┘
typ └──────────┘ └┘ └───┘ ┴└────┘ └──────────┘ └┘ └──┘
278 by simpa [(multiset.map_eq_map subtype.val_injective).symm, rel_associated_iff_map_eq_map.symm]
id └─────────────────┘ └───────────────────┘
src └─────┘ └─────────────────┘┴└───────────────────┘└──────┘ └─
typ └─────┘ └─────────────────┘┴└───────────────────┘└──────┘└────────────────────────────────┘└─
doc └─────┘ ┴ └──────┘ └─
txt └─────┘ ┴ └──────┘ └─
par └─────┘ ┴ └──────┘ └─
pid ┴┴ ┴ └──────┘ ┴└
st └─────────────────────────────────────────────────────────────────────────────────────────────
279
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
280 def factors (a : associates α) : factor_set α :=
id └────────┘ ┴ └────────┘ ┴
src └────────┘ └────────┘
typ └────────┘ ┴ └────────┘ ┴
doc └────────┘
281 begin
st └─────
282 refine (if h : a = 0 then ⊤ else
id └┘ ┴ ┴
src └─────┘ └┘└───┘ ┴┴└──────┘┴└─────
typ └─────┘ └┘└───┘ ┴┴└──────┘┴└─────
doc └─────┘ └───┘ ┴ └──────┘ └─────
txt └─────┘ └───┘ ┴ └──────┘ └─────
par └─────┘ └───┘ ┴ └──────┘ └─────
pid ┴ └───┘ ┴ └──────┘ └─────
st ───────────────────────────────────
283 quotient.hrec_on a (λx h, some $ factors' x (mt mk_eq_zero_iff_eq_zero.2 h)) _ h),
id └──────────────┘ ┴ └──┘ └──────┘ └┘ └────────────────────┘
src ───┘└──────────────┘┴ ┴ └───┘└──┘┴ ┴└──────┘┴ ┴ └┘┴└────────────────────┘└─┘ └───┘ ┴
typ ───┘└──────────────┘┴┴┴ └───┘└──┘┴ ┴└──────┘┴ ┴ └┘┴└────────────────────┘└─┘ └───┘ ┴
doc ───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └─┘ └───┘ ┴
txt ───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └─┘ └───┘ ┴
par ───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └─┘ └───┘ ┴
pid ───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └─┘ └───┘ ┴
st ────────────────────────────────────────────────────────────────────────────────────┘└─
284
st ─
285 assume a b hab,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └────────────┘
st ───────────────┘└─
286 apply function.hfunext,
id └──────────────┘
src └────┘└──────────────┘
typ └────┘└──────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────┘└─
287 { have : a ~ᵤ 0 ↔ b ~ᵤ 0, from
id ┴ └┘ ┴
src └─────┘ ┴└┘└─┘ ┴ ┴ └┘ └────
typ └─────┘┴┴└┘└─┘ ┴┴┴ └┘ └────
doc └─────┘ ┴ └─┘ ┴ ┴ └┘ └────
txt └─────┘ ┴ └─┘ ┴ ┴ └┘ └────
par └─────┘ ┴ └─┘ ┴ ┴ └┘ └────
pid └───┘└┘ ┴ └─┘ ┴ ┴ ┴┴ └────
st ───┘└────────────────────┘└──────
288 iff.intro (assume ha0, hab.symm.trans ha0) (assume hb0, hab.trans hb0),
id └───────┘ └────────────┘ └───────┘
src ─────┘└───────┘┴ └────┘└────────────┘┴ └┘ └────┘└───────┘┴ ┴
typ ─────┘└───────┘┴ └────┘└────────────┘┴ └┘ └────┘└───────┘┴ ┴
doc ─────┘ ┴ └────┘ ┴ └┘ └────┘ ┴ ┴
txt ─────┘ ┴ └────┘ ┴ └┘ └────┘ ┴ ┴
par ─────┘ ┴ └────┘ ┴ └┘ └────┘ ┴ ┴
pid ─────┘ ┴ └────┘ ┴ └┘ └────┘ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────┘└─
289 simp [quotient_mk_eq_mk, mk_eq_zero_iff_eq_zero, (associated_zero_iff_eq_zero _).symm, this] },
id └───────────────┘ └────────────────────┘ └─────────────────────────┘ └──┘
src └────┘└───────────────┘└┘└────────────────────┘└┘ └─────────────────────────┘└────────┘ └┘
typ └────┘└───────────────┘└┘└────────────────────┘└┘ └─────────────────────────┘└────────┘└──┘└┘
doc └────┘ └┘ └┘ └────────┘ └┘
txt └────┘ └┘ └┘ └────────┘ └┘
par └────┘ └┘ └┘ └────────┘ └┘
pid ┴┴ └┘ └┘ └────────┘ ┴┴
st ────────────────────────────────────────────────────────────────────────────────────────────────┘└┘└
290 exact (assume ha hb eq, heq_of_eq $ congr_arg some $ factors'_cong _ _ hab)
id └───────┘ └───────┘ └──┘ └───────────┘ └─┘
src └────┘ └─────────┘└───────┘┴ ┴└───────┘┴└──┘┴ ┴└───────────┘└───┘ └┘
typ └────┘ └─────────┘└───────┘┴ ┴└───────┘┴└──┘┴ ┴└───────────┘└───┘└─┘└┘
doc └────┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ └───┘ └┘
txt └────┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ └───┘ └┘
par └────┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ └───┘ └┘
pid ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴┴
st ─────────────────────────────────────────────────────────────────────────────┘
291 end
st └─┘
292
293 @[simp] theorem factors_0 : (0 : associates α).factors = ⊤ :=
id └────────┘ ┴ └─────┘ ┴ ┴
src └────────┘ └─────┘ ┴ ┴
typ └────────┘ ┴ └─────┘ ┴ ┴
doc └──┘
294 dif_pos rfl
id └─────┘ └─┘
src └─────┘ └─┘
typ └─────┘ └─┘
295
296 @[simp] theorem factors_mk (a : α) (h : a ≠ 0) : (associates.mk a).factors = factors' a h :=
id ┴ ┴ ┴ └───────────┘ ┴ └─────┘ ┴ └──────┘ ┴ ┴
src ┴ └───────────┘ └─────┘ ┴ └──────┘
typ ┴ ┴ ┴ └───────────┘ ┴ └─────┘ ┴ └──────┘ ┴ ┴
doc └──┘
297 dif_neg (mt mk_eq_zero_iff_eq_zero.1 h)
id └─────┘ └┘ └────────────────────┘┴ ┴
src └─────┘ └┘ └────────────────────┘┴
typ └─────┘ └┘ └────────────────────┘┴ ┴
298
299 def factor_set.prod : factor_set α → associates α
id └────────┘ ┴ ┴ └────────┘ ┴
src └────────┘ └────────┘
typ └────────┘ ┴ ┴ └────────┘ ┴
doc └────────┘
300 | none := 0
id └──┘
src └──┘
typ └──┘
301 | (some s) := (s.map subtype.val).prod
id └──┘ ┴ └──┘ └─────────┘ └──┘
src └──┘ └──┘ └─────────┘ └──┘
typ └──┘ ┴ └──┘ └─────────┘ └──┘
doc └──┘ └──┘
302
303 @[simp] theorem prod_top : (⊤ : factor_set α).prod = 0 := rfl
id ┴ └────────┘ ┴ └──┘ ┴ └─┘
src ┴ └────────┘ └──┘ ┴ └─┘
typ ┴ └────────┘ ┴ └──┘ ┴ └─┘
doc └──┘ └────────┘
304
305 @[simp] theorem prod_coe {s : multiset { a : associates α // irreducible a }} :
id └──────┘ ┴ └────────┘ ┴ └─────────┘ ┴
src └──────┘ ┴ └────────┘ └─────────┘
typ └──────┘ ┴ └────────┘ ┴ └─────────┘ ┴
doc └──┘ └──────┘ └─────────┘
306 (s : factor_set α).prod = (s.map subtype.val).prod :=
id ┴ └────────┘ ┴ └──┘ ┴ ┴└──┘ └─────────┘ └──┘
src └────────┘ └──┘ ┴ └──┘ └─────────┘ └──┘
typ ┴ └────────┘ ┴ └──┘ ┴ ┴└──┘ └─────────┘ └──┘
doc └────────┘ └──┘ └──┘
307 rfl
id └─┘
src └─┘
typ └─┘
308
309 theorem prod_factors : ∀(s : factor_set α), s.prod.factors = s
id ┴ └────────┘ ┴ ┴└───┘└──────┘ ┴ ┴
src └────────┘ └───┘└──────┘ ┴
typ ┴ └────────┘ ┴ ┴└───┘└──────┘ ┴ ┴
doc └────────┘
310 | none := by simp [factor_set.prod]; refl
id └──┘ └─────────────┘
src └──┘ └────┘└─────────────┘┴ └───┘
typ └──┘ └────┘└─────────────┘┴ └───┘
doc └────┘ ┴ └───┘
txt └────┘ ┴ └───┘
par └────┘ ┴ └───┘
pid ┴┴ ┴ ┴
st └────────────────────────────┘
311 | (some s) :=
id └──┘
src └──┘
typ └──┘
312 begin
st └─────
313 unfold factor_set.prod,
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
txt └────────────────────┘
par └────────────────────┘
pid └──────────────┘
st ─────────────────────────┘└─
314 generalize eq_a : (s.map subtype.val).prod = a,
id └───┘ └─────────┘
src └────────────────┘ └───┘┴└─────────┘└─────┘ ┴
typ └────────────────┘ └───┘┴└─────────┘└─────┘ ┴
doc └────────────────┘ └───┘┴ └─────┘ ┴
txt └────────────────┘ ┴ └─────┘ ┴
par └────────────────┘ ┴ └─────┘ ┴
pid └───┘└┘┴ ┴ └─────┘ ┴
st ─────────────────────────────────────────────────┘└─
315 rcases a with ⟨a⟩,
id ┴
src └─────┘ └───────┘
typ └─────┘┴└───────┘
doc └─────┘ └───────┘
txt └─────┘ └───────┘
par └─────┘ └───────┘
pid ┴ └───────┘
st ────────────────────┘└─
316 rw quot_mk_eq_mk at *,
id └───────────┘
src └─┘└───────────┘└───┘
typ └─┘└───────────┘└───┘
doc └─┘ └───┘
txt └─┘ └───┘
par └─┘ └───┘
pid ┴ └───┘
st ────────────────────────┘└─
317
st ─
318 have : (s.map subtype.val).prod ≠ 0, from assume ha,
id └───┘ └─────────┘ ┴
src └─────┘ └───┘┴└─────────┘└─────┘┴└┘ └───┘ └────
typ └─────┘ └───┘┴└─────────┘└─────┘┴└┘ └───┘ └────
doc └─────┘ └───┘┴ └─────┘ └┘ └───┘ └────
txt └─────┘ ┴ └─────┘ └┘ └───┘ └────
par └─────┘ ┴ └─────┘ └┘ └───┘ └────
pid └───┘└┘ ┴ └─────┘ ┴┴ └───┘ └────
st ──────────────────────────────────────┘└─────────────────
319 let ⟨⟨a, ha⟩, h, eq⟩ := multiset.mem_map.1 (prod_eq_zero_iff.1 ha) in
id └┘ └──────────────┘ └──────────────┘
src ─────┘ ┴ └┘ └─┘ └┘└┘└───┘└──────────────┘└─┘ └──────────────┘└─┘ └────
typ ─────┘ ┴ └┘ └─┘ └┘└┘└───┘└──────────────┘└─┘ └──────────────┘└─┘ └────
doc ─────┘ ┴ └┘ └─┘ └┘ └───┘ └─┘ └─┘ └────
txt ─────┘ ┴ └┘ └─┘ └┘ └───┘ └─┘ └─┘ └────
par ─────┘ ┴ └┘ └─┘ └┘ └───┘ └─┘ └─┘ └────
pid ─────┘ ┴ └┘ └─┘ └┘ └───┘ └─┘ └─┘ └────
st ────────────────────────────────────────────────────────────────────────────
320 have irreducible (0 : associates α), from eq ▸ ha,
id └────────┘ ┴ ┴
src ─────┘ └───────────┘ └──┘└────────┘┴ └──────┘ ┴┴┴ └─
typ ─────┘ └───────────┘ └──┘└────────┘┴┴└──────┘ ┴┴┴ └─
doc ─────┘ └───────────┘ └──┘ ┴ └──────┘ ┴ ┴ └─
txt ─────┘ └───────────┘ └──┘ ┴ └──────┘ ┴ ┴ └─
par ─────┘ └───────────┘ └──┘ ┴ └──────┘ ┴ ┴ └─
pid ─────┘ └───────────┘ └──┘ ┴ └──────┘ ┴ ┴ └─
st ─────────────────────────────────────────────────────────
321 not_irreducible_zero ((irreducible_mk_iff _).1 this),
id └──────────────────┘ └────────────────┘
src ─────┘└──────────────────┘┴ └────────────────┘└────┘ ┴
typ ─────┘└──────────────────┘┴ └────────────────┘└────┘ ┴
doc ─────┘ ┴ └────┘ ┴
txt ─────┘ ┴ └────┘ ┴
par ─────┘ ┴ └────┘ ┴
pid ─────┘ ┴ └────┘ ┴
st ─────────────────────────────────────────────────────────┘└─
322 have ha : a ≠ 0, by simp [*] at *,
id ┴
src └────────┘ ┴ └┘ └───────────┘
typ └────────┘┴┴ └┘ └───────────┘
doc └────────┘ ┴ └┘ └───────────┘
txt └────────┘ ┴ └┘ └───────────┘
par └────────┘ ┴ └┘ └───────────┘
pid └─────┘└─┘ ┴ ┴┴ ┴└─┘┴└──┘
st ──────────────────┘ └─
323 suffices : (unique_factorization_domain.factors a).map associates.mk = s.map subtype.val,
id └─────────────────────────────────┘ ┴ └───────────┘ └───┘ └─────────┘
src └─────────┘ └─────────────────────────────────┘┴ └────┘└───────────┘┴ ┴└───┘┴└─────────┘
typ └─────────┘ └─────────────────────────────────┘┴┴└────┘└───────────┘┴ ┴└───┘┴└─────────┘
doc └─────────┘ ┴ └────┘ ┴ ┴└───┘┴
txt └─────────┘ ┴ └────┘ ┴ ┴ ┴
par └─────────┘ ┴ └────┘ ┴ ┴ ┴
pid └───────┘└┘ ┴ └────┘ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────────────────────┘└─
324 { rw [factors_mk a ha],
id └────────┘ ┴ └┘
src └──┘└────────┘┴ ┴ ┴
typ └──┘└────────┘┴┴┴└┘┴
doc └──┘ ┴ ┴ ┴
txt └──┘ ┴ ┴ ┴
par └──┘ ┴ ┴ ┴
pid └┘ ┴ ┴ ┴
st ─────┘└─────────────────┘└──
325 apply congr_arg some _,
id └───────┘ └──┘
src └────┘└───────┘┴└──┘└┘
typ └────┘└───────┘┴└──┘└┘
doc └────┘ ┴ └┘
txt └────┘ ┴ └┘
par └────┘ ┴ └┘
pid ┴ ┴ └┘
st ───────────────────────────┘└─
326 simpa [(multiset.map_eq_map subtype.val_injective).symm] },
id └─────────────────┘ └───────────────────┘
src └─────┘ └─────────────────┘┴└───────────────────┘└──────┘
typ └─────┘ └─────────────────┘┴└───────────────────┘└──────┘
doc └─────┘ ┴ └──────┘
txt └─────┘ ┴ └──────┘
par └─────┘ ┴ └──────┘
pid ┴┴ ┴ └─────┘┴
st ──────────────────────────────────────────────────────────────┘└┘└
327
st ─
328 refine unique'
id └─────┘
src └─────┘└─────┘└
typ └─────┘└─────┘└
doc └─────┘ └
txt └─────┘ └
par └─────┘ └
pid ┴ └
st ───────────────────
329 (forall_map_mk_factors_irreducible _ ha)
id └───────────────────────────────┘ └┘
src ─────┘ └───────────────────────────────┘└─┘ └─
typ ─────┘ └───────────────────────────────┘└─┘└┘└─
doc ─────┘ └─┘ └─
txt ─────┘ └─┘ └─
par ─────┘ └─┘ └─
pid ─────┘ └─┘ └─
st ───────────────────────────────────────────────
330 (assume a ha, let ⟨⟨x, hx⟩, ha, eq⟩ := multiset.mem_map.1 ha in eq ▸ hx)
id └┘ └┘ └──────────────┘
src ─────┘ └─────┘ ┴ └┘ └─┘ └┘└┘└───┘└──────────────┘└─┘ └──┘ ┴ ┴ └─
typ ─────┘ └─────┘ ┴ └┘└┘└─┘ └┘└┘└───┘└──────────────┘└─┘ └──┘ ┴ ┴ └─
doc ─────┘ └─────┘ ┴ └┘ └─┘ └┘ └───┘ └─┘ └──┘ ┴ ┴ └─
txt ─────┘ └─────┘ ┴ └┘ └─┘ └┘ └───┘ └─┘ └──┘ ┴ ┴ └─
par ─────┘ └─────┘ ┴ └┘ └─┘ └┘ └───┘ └─┘ └──┘ ┴ ┴ └─
pid ─────┘ └─────┘ ┴ └┘ └─┘ └┘ └───┘ └─┘ └──┘ ┴ ┴ └─
st ───────────────────────────────────────────────────────────────────────────────
331 _,
src ──────┘
typ ──────┘
doc ──────┘
txt ──────┘
par ──────┘
pid ──────┘
st ──────┘└─
332 rw [prod_mk, eq_a, mk_eq_mk_iff_associated],
id └─────┘ └──┘ └─────────────────────┘
src └──┘└─────┘└┘ └┘└─────────────────────┘┴
typ └──┘└─────┘└┘└──┘└┘└─────────────────────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ──────────────┘└────┘└───────────────────────┘└──
333 exact factors_prod ha
id └──────────┘ └┘
src └────┘└──────────┘┴ └
typ └────┘└──────────┘┴└┘└
doc └────┘ ┴ └
txt └────┘ ┴ └
par └────┘ ┴ └
pid ┴ ┴ └
st ──────────────────────────
334 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
335
336 theorem factors_prod (a : associates α) : a.factors.prod = a :=
id └────────┘ ┴ ┴└──────┘└───┘ ┴ ┴
src └────────┘ └──────┘└───┘ ┴
typ └────────┘ ┴ ┴└──────┘└───┘ ┴ ┴
337 quotient.induction_on a $ assume a, decidable.by_cases
id └───────────────────┘ ┴ ┴ └────────────────┘
src └───────────────────┘ └────────────────┘
typ └───────────────────┘ ┴ ┴ └────────────────┘
338 (assume : associates.mk a = 0, by simp [quotient_mk_eq_mk, this])
id └───────────┘ ┴ ┴ └───────────────┘ └──┘
src └───────────┘ ┴ └────┘└───────────────┘└┘ ┴
typ └───────────┘ ┴ ┴ └────┘└───────────────┘└┘└──┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └─────────────────────────────┘
339 (assume : associates.mk a ≠ 0,
id └───────────┘ ┴ ┴
src └───────────┘ ┴
typ └───────────┘ ┴ ┴
340 have a ≠ 0, by simp * at *,
id ┴ ┴
src ┴ └─────────┘
typ ┴ ┴ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid ┴┴┴└──┘
st └──────────┘
341 by simp [this, quotient_mk_eq_mk, prod_mk, mk_eq_mk_iff_associated.2 (factors_prod this)])
id └──┘ └───────────────┘ └─────┘ └─────────────────────┘ └──────────┘ └──┘
src └────┘ └┘└───────────────┘└┘└─────┘└┘└─────────────────────┘└─┘ └──────────┘┴ └┘
typ └────┘└──┘└┘└───────────────┘└┘└─────┘└┘└─────────────────────┘└─┘ └──────────┘┴└──┘└┘
doc └────┘ └┘ └┘ └┘ └─┘ ┴ └┘
txt └────┘ └┘ └┘ └┘ └─┘ ┴ └┘
par └────┘ └┘ └┘ └┘ └─┘ ┴ └┘
pid ┴┴ └┘ └┘ └┘ └─┘ ┴ └┘
st └─────────────────────────────────────────────────────────────────────────────────────┘
342
343 theorem eq_of_factors_eq_factors {a b : associates α} (h : a.factors = b.factors) : a = b :=
id └────────┘ ┴ ┴└──────┘ ┴ ┴└──────┘ ┴ ┴ ┴
src └────────┘ └──────┘ ┴ └──────┘ ┴
typ └────────┘ ┴ ┴└──────┘ ┴ ┴└──────┘ ┴ ┴ ┴
344 have a.factors.prod = b.factors.prod, by rw h,
id ┴└──────┘└───┘ ┴ ┴└──────┘└───┘ ┴
src └──────┘└───┘ ┴ └──────┘└───┘ └─┘
typ ┴└──────┘└───┘ ┴ ┴└──────┘└───┘ └─┘┴
doc └─┘
txt └─┘
par └─┘
pid ┴
st └───┘
345 by rwa [factors_prod, factors_prod] at this
id └──────────┘ └──────────┘
src └───┘└──────────┘└┘└──────────┘└─────────
typ └───┘└──────────┘└┘└──────────┘└─────────
doc └───┘ └┘ └─────────
txt └───┘ └┘ └─────────
par └───┘ └┘ └─────────
pid └┘ └┘ ┴└──────┘└
st └────────────────┘└────────────┘┴└────────
346
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
347 theorem eq_of_prod_eq_prod {a b : factor_set α} (h : a.prod = b.prod) : a = b :=
id └────────┘ ┴ ┴└───┘ ┴ ┴└───┘ ┴ ┴ ┴
src └────────┘ └───┘ ┴ └───┘ ┴
typ └────────┘ ┴ ┴└───┘ ┴ ┴└───┘ ┴ ┴ ┴
doc └────────┘
348 have a.prod.factors = b.prod.factors, by rw h,
id ┴└───┘└──────┘ ┴ ┴└───┘└──────┘ ┴
src └───┘└──────┘ ┴ └───┘└──────┘ └─┘
typ ┴└───┘└──────┘ ┴ ┴└───┘└──────┘ └─┘┴
doc └─┘
txt └─┘
par └─┘
pid ┴
st └───┘
349 by rwa [prod_factors, prod_factors] at this
id └──────────┘ └──────────┘
src └───┘└──────────┘└┘└──────────┘└─────────
typ └───┘└──────────┘└┘└──────────┘└─────────
doc └───┘ └┘ └─────────
txt └───┘ └┘ └─────────
par └───┘ └┘ └─────────
pid └┘ └┘ ┴└──────┘└
st └────────────────┘└────────────┘┴└────────
350
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
351 @[simp] theorem prod_add : ∀(a b : factor_set α), (a + b).prod = a.prod * b.prod
id ┴ └────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴└───┘ ┴ ┴└───┘
src └────────┘ ┴ └──┘ ┴ └───┘ ┴ └───┘
typ ┴ └────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴└───┘ ┴ ┴└───┘
doc └──┘ └────────┘
352 | none b := show (⊤ + b).prod = (⊤:factor_set α).prod * b.prod, by simp
id └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ └────────┘ ┴ └──┘ ┴ └───┘
src └──┘ ┴ ┴ └──┘ ┴ ┴ └────────┘ └──┘ ┴ └───┘ └───┘
typ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ └────────┘ ┴ └──┘ ┴ └───┘ └───┘
doc └────────┘ └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
353 | a none := show (a + ⊤).prod = a.prod * (⊤:factor_set α).prod, by simp
id ┴ └──┘ ┴ ┴ └──┘ ┴ └───┘ ┴ ┴ └────────┘ ┴ └──┘
src └──┘ ┴ ┴ └──┘ ┴ └───┘ ┴ ┴ └────────┘ └──┘ └───┘
typ ┴ └──┘ ┴ ┴ └──┘ ┴ └───┘ ┴ ┴ └────────┘ ┴ └──┘ └───┘
doc └────────┘ └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
354 | (some a) (some b) :=
id ┴ └──┘ ┴
src └──┘
typ ┴ └──┘ ┴
355 show (↑a + ↑b:factor_set α).prod = (↑a:factor_set α).prod * (↑b:factor_set α).prod,
id ┴ ┴ ┴ └────────┘ ┴ └──┘ ┴ ┴ └────────┘ ┴ └──┘ ┴ ┴ └────────┘ ┴ └──┘
src ┴ ┴ ┴ └────────┘ └──┘ ┴ ┴ └────────┘ └──┘ ┴ ┴ └────────┘ └──┘
typ ┴ ┴ ┴ └────────┘ ┴ └──┘ ┴ ┴ └────────┘ ┴ └──┘ ┴ ┴ └────────┘ ┴ └──┘
doc └────────┘ └────────┘ └────────┘
356 by rw [factor_set.coe_add, prod_coe, prod_coe, prod_coe, multiset.map_add, multiset.prod_add]
id └────────────────┘ └──────┘ └──────┘ └──────┘ └──────────────┘ └───────────────┘
src └──┘└────────────────┘└┘└──────┘└┘└──────┘└┘└──────┘└┘└──────────────┘└┘└───────────────┘└─
typ └──┘└────────────────┘└┘└──────┘└┘└──────┘└┘└──────┘└┘└──────────────┘└┘└───────────────┘└─
doc └──┘ └┘ └┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ └┘ └┘ ┴└
st └─────────────────────┘└────────┘└────────┘└────────┘└────────────────┘└─────────────────┘┴└
357
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
358 theorem prod_mono : ∀{a b : factor_set α}, a ≤ b → a.prod ≤ b.prod
id ┴ └────────┘ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴└───┘
src └────────┘ ┴ └───┘ ┴ └───┘
typ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴└───┘
doc └────────┘
359 | none b h := have b = ⊤, from top_unique h, by rw [this, prod_top]; exact le_refl _
id └──┘ ┴ ┴ ┴ ┴ └────────┘ └──┘ └──────┘ └─────┘
src └──┘ ┴ ┴ └────────┘ └──┘ └┘└──────┘┴ └────┘└─────┘└─┘
typ └──┘ ┴ ┴ ┴ ┴ └────────┘ └──┘└──┘└┘└──────┘┴ └────┘└─────┘└─┘
doc └──┘ └┘ ┴ └────┘ └─┘
txt └──┘ └┘ ┴ └────┘ └─┘
par └──┘ └┘ ┴ └────┘ └─┘
pid └┘ └┘ ┴ ┴ └┘┴
st └───────┘└────────┘┴└────────────────┘
360 | a none h := show a.prod ≤ (⊤ : factor_set α).prod, by simp; exact le_top
id ┴ └──┘ └───┘ ┴ ┴ └────────┘ ┴ └──┘ └────┘
src └──┘ └───┘ ┴ ┴ └────────┘ └──┘ └──┘ └────┘└────┘┴
typ ┴ └──┘ └───┘ ┴ ┴ └────────┘ ┴ └──┘ └──┘ └────┘└────┘┴
doc └────────┘ └──┘ └────┘ ┴
txt └──┘ └────┘ ┴
par └──┘ └────┘ ┴
pid ┴ ┴
st └──────────────────┘
361 | (some a) (some b) h := prod_le_prod $ multiset.map_le_map $ with_top.coe_le_coe.1 $ h
id └──┘ ┴ └──────────┘ └─────────────────┘ └─────────────────┘┴
src └──┘ └──────────┘ └─────────────────┘ └─────────────────┘┴
typ └──┘ ┴ └──────────┘ └─────────────────┘ └─────────────────┘┴
362
363 @[simp] theorem factors_mul (a b : associates α) : (a * b).factors = a.factors + b.factors :=
id └────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴└──────┘ ┴ ┴└──────┘
src └────────┘ ┴ └─────┘ ┴ └──────┘ ┴ └──────┘
typ └────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴└──────┘ ┴ ┴└──────┘
doc └──┘
364 eq_of_prod_eq_prod $ eq_of_factors_eq_factors $
id └────────────────┘ └──────────────────────┘
src └────────────────┘ └──────────────────────┘
typ └────────────────┘ └──────────────────────┘
365 by rw [prod_add, factors_prod, factors_prod, factors_prod]
id └──────┘ └──────────┘ └──────────┘ └──────────┘
src └──┘└──────┘└┘└──────────┘└┘└──────────┘└┘└──────────┘└─
typ └──┘└──────┘└┘└──────────┘└┘└──────────┘└┘└──────────┘└─
doc └──┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ ┴└
st └───────────┘└────────────┘└────────────┘└────────────┘┴└
366
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
367 theorem factors_mono : ∀{a b : associates α}, a ≤ b → a.factors ≤ b.factors
id ┴ └────────┘ ┴ ┴ ┴ ┴ ┴└──────┘ ┴ ┴└──────┘
src └────────┘ ┴ └──────┘ ┴ └──────┘
typ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴└──────┘ ┴ ┴└──────┘
368 | s t ⟨d, rfl⟩ := by rw [factors_mul] ; exact le_add_of_nonneg_right' bot_le
id └─┘ └─────────┘ └─────────────────────┘ └────┘
src └─┘ └──┘└─────────┘└┘ └────┘└─────────────────────┘┴└────┘└
typ └─┘ └──┘└─────────┘└┘ └────┘└─────────────────────┘┴└────┘└
doc └──┘ └┘ └────┘ ┴ └
txt └──┘ └┘ └────┘ ┴ └
par └──┘ └┘ └────┘ ┴ └
pid └┘ ┴┴ ┴ ┴ └
st └──────────────┘┴└───────────────────────────────────────
369
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
370 theorem factors_le {a b : associates α} : a.factors ≤ b.factors ↔ a ≤ b :=
id └────────┘ ┴ ┴└──────┘ ┴ ┴└──────┘ ┴ ┴ ┴ ┴
src └────────┘ └──────┘ ┴ └──────┘ ┴ ┴
typ └────────┘ ┴ ┴└──────┘ ┴ ┴└──────┘ ┴ ┴ ┴ ┴
371 iff.intro
id └───────┘
src └───────┘
typ └───────┘
372 (assume h, have a.factors.prod ≤ b.factors.prod, from prod_mono h,
id ┴ ┴└──────┘└───┘ ┴ ┴└──────┘└───┘ └───────┘ ┴
src └──────┘└───┘ ┴ └──────┘└───┘ └───────┘
typ ┴ ┴└──────┘└───┘ ┴ ┴└──────┘└───┘ └───────┘ ┴
373 by rwa [factors_prod, factors_prod] at this)
id └──────────┘ └──────────┘
src └───┘└──────────┘└┘└──────────┘└───────┘
typ └───┘└──────────┘└┘└──────────┘└───────┘
doc └───┘ └┘ └───────┘
txt └───┘ └┘ └───────┘
par └───┘ └┘ └───────┘
pid └┘ └┘ ┴└──────┘
st └────────────────┘└────────────┘┴└──────┘
374 factors_mono
id └──────────┘
src └──────────┘
typ └──────────┘
375
376 theorem prod_le {a b : factor_set α} : a.prod ≤ b.prod ↔ a ≤ b :=
id └────────┘ ┴ ┴└───┘ ┴ ┴└───┘ ┴ ┴ ┴ ┴
src └────────┘ └───┘ ┴ └───┘ ┴ ┴
typ └────────┘ ┴ ┴└───┘ ┴ ┴└───┘ ┴ ┴ ┴ ┴
doc └────────┘
377 iff.intro
id └───────┘
src └───────┘
typ └───────┘
378 (assume h, have a.prod.factors ≤ b.prod.factors, from factors_mono h,
id ┴ ┴└───┘└──────┘ ┴ ┴└───┘└──────┘ └──────────┘ ┴
src └───┘└──────┘ ┴ └───┘└──────┘ └──────────┘
typ ┴ ┴└───┘└──────┘ ┴ ┴└───┘└──────┘ └──────────┘ ┴
379 by rwa [prod_factors, prod_factors] at this)
id └──────────┘ └──────────┘
src └───┘└──────────┘└┘└──────────┘└───────┘
typ └───┘└──────────┘└┘└──────────┘└───────┘
doc └───┘ └┘ └───────┘
txt └───┘ └┘ └───────┘
par └───┘ └┘ └───────┘
pid └┘ └┘ ┴└──────┘
st └────────────────┘└────────────┘┴└──────┘
380 prod_mono
id └───────┘
src └───────┘
typ └───────┘
381
382 instance : has_sup (associates α) := ⟨λa b, (a.factors ⊔ b.factors).prod⟩
id └─────┘ └────────┘ ┴ ┴ ┴ ┴└──────┘ ┴ ┴└──────┘ └──┘
src └─────┘ └────────┘ └──────┘ ┴ └──────┘ └──┘
typ └─────┘ └────────┘ ┴ ┴ ┴ ┴└──────┘ ┴ ┴└──────┘ └──┘
doc └─────┘
383 instance : has_inf (associates α) := ⟨λa b, (a.factors ⊓ b.factors).prod⟩
id └─────┘ └────────┘ ┴ ┴ ┴ ┴└──────┘ ┴ ┴└──────┘ └──┘
src └─────┘ └────────┘ └──────┘ ┴ └──────┘ └──┘
typ └─────┘ └────────┘ ┴ ┴ ┴ ┴└──────┘ ┴ ┴└──────┘ └──┘
doc └─────┘
384
385 instance : bounded_lattice (associates α) :=
id └─────────────┘ └────────┘ ┴
src └─────────────┘ └────────┘
typ └─────────────┘ └────────┘ ┴
doc └─────────────┘
386 { sup := (⊔),
id ┴
src ┴
typ ┴
387 inf := (⊓),
id ┴
src ┴
typ ┴
388 sup_le :=
389 assume a b c hac hbc, factors_prod c ▸ prod_mono (sup_le (factors_mono hac) (factors_mono hbc)),
id ┴ ┴ ┴ └─┘ └─┘ └──────────┘ ┴ ┴ └───────┘ └────┘ └──────────┘ └─┘ └──────────┘ └─┘
src └──────────┘ ┴ └───────┘ └────┘ └──────────┘ └──────────┘
typ ┴ ┴ ┴ └─┘ └─┘ └──────────┘ ┴ ┴ └───────┘ └────┘ └──────────┘ └─┘ └──────────┘ └─┘
390 le_sup_left := assume a b,
id ┴ ┴
typ ┴ ┴
391 le_trans (le_of_eq (factors_prod a).symm) $ prod_mono $ le_sup_left,
id └──────┘ └──────┘ └──────────┘ ┴ └──┘ └───────┘ └─────────┘
src └──────┘ └──────┘ └──────────┘ └──┘ └───────┘ └─────────┘
typ └──────┘ └──────┘ └──────────┘ ┴ └──┘ └───────┘ └─────────┘
392 le_sup_right := assume a b,
id ┴ ┴
typ ┴ ┴
393 le_trans (le_of_eq (factors_prod b).symm) $ prod_mono $ le_sup_right,
id └──────┘ └──────┘ └──────────┘ ┴ └──┘ └───────┘ └──────────┘
src └──────┘ └──────┘ └──────────┘ └──┘ └───────┘ └──────────┘
typ └──────┘ └──────┘ └──────────┘ ┴ └──┘ └───────┘ └──────────┘
394 le_inf :=
395 assume a b c hac hbc, factors_prod a ▸ prod_mono (le_inf (factors_mono hac) (factors_mono hbc)),
id ┴ ┴ ┴ └─┘ └─┘ └──────────┘ ┴ ┴ └───────┘ └────┘ └──────────┘ └─┘ └──────────┘ └─┘
src └──────────┘ ┴ └───────┘ └────┘ └──────────┘ └──────────┘
typ ┴ ┴ ┴ └─┘ └─┘ └──────────┘ ┴ ┴ └───────┘ └────┘ └──────────┘ └─┘ └──────────┘ └─┘
396 inf_le_left := assume a b,
id ┴ ┴
typ ┴ ┴
397 le_trans (prod_mono inf_le_left) (le_of_eq (factors_prod a)),
id └──────┘ └───────┘ └─────────┘ └──────┘ └──────────┘ ┴
src └──────┘ └───────┘ └─────────┘ └──────┘ └──────────┘
typ └──────┘ └───────┘ └─────────┘ └──────┘ └──────────┘ ┴
398 inf_le_right := assume a b,
id ┴ ┴
typ ┴ ┴
399 le_trans (prod_mono inf_le_right) (le_of_eq (factors_prod b)),
id └──────┘ └───────┘ └──────────┘ └──────┘ └──────────┘ ┴
src └──────┘ └───────┘ └──────────┘ └──────┘ └──────────┘
typ └──────┘ └───────┘ └──────────┘ └──────┘ └──────────┘ ┴
400 .. associates.partial_order,
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
401 .. associates.lattice.order_top,
id └──────────────────────────┘
src └──────────────────────────┘
typ └──────────────────────────┘
402 .. associates.lattice.order_bot }
id └──────────────────────────┘
src └──────────────────────────┘
typ └──────────────────────────┘
403
404 lemma sup_mul_inf (a b : associates α) : (a ⊔ b) * (a ⊓ b) = a * b :=
id └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴ ┴ ┴ ┴
typ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
405 show (a.factors ⊔ b.factors).prod * (a.factors ⊓ b.factors).prod = a * b,
id ┴└──────┘ ┴ ┴└──────┘ └──┘ ┴ ┴└──────┘ ┴ ┴└──────┘ └──┘ ┴ ┴ ┴ ┴
src └──────┘ ┴ └──────┘ └──┘ ┴ └──────┘ ┴ └──────┘ └──┘ ┴ ┴
typ ┴└──────┘ ┴ ┴└──────┘ └──┘ ┴ ┴└──────┘ ┴ ┴└──────┘ └──┘ ┴ ┴ ┴ ┴
406 begin
st └─────
407 refine eq_of_factors_eq_factors _,
id └──────────────────────┘
src └─────┘└──────────────────────┘└┘
typ └─────┘└──────────────────────┘└┘
doc └─────┘ └┘
txt └─────┘ └┘
par └─────┘ └┘
pid ┴ └┘
st ──────────────────────────────────┘└─
408 rw [← prod_add, prod_factors, factors_mul, factor_set.sup_add_inf_eq_add]
id └──────┘ └──────────┘ └─────────┘ └───────────────────────────┘
src └────┘└──────┘└┘└──────────┘└┘└─────────┘└┘└───────────────────────────┘└┘
typ └────┘└──────┘└┘└──────────┘└┘└─────────┘└┘└───────────────────────────┘└┘
doc └────┘ └┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘ └┘
pid └──┘ └┘ └┘ └┘ ┴┴
st ───────────────┘└────────────┘└───────────┘└─────────────────────────────┘┴┴
409 end
st └─┘
410
411 end associates
412
413 section
414 open associates unique_factorization_domain lattice
415
416 /-- `to_gcd_domain` constructs a GCD domain out of a unique factorization domain over a normalization
417 domain. -/
418 def unique_factorization_domain.to_gcd_domain
419 (α : Type*) [normalization_domain α] [unique_factorization_domain α] [decidable_eq (associates α)] :
id └──────────────────┘ ┴ └─────────────────────────┘ ┴ └──────────┘ └────────┘ ┴
src └──────────────────┘ └─────────────────────────┘ └──────────┘ └────────┘
typ └──────────────────┘ ┴ └─────────────────────────┘ ┴ └──────────┘ └────────┘ ┴
doc └──────────────────┘ └─────────────────────────┘
420 gcd_domain α :=
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
doc └────────┘
421 { gcd := λa b, (associates.mk a ⊓ associates.mk b).out,
id ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ └─┘
src └───────────┘ ┴ └───────────┘ └─┘
typ ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ └─┘
422 lcm := λa b, (associates.mk a ⊔ associates.mk b).out,
id ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ └─┘
src └───────────┘ ┴ └───────────┘ └─┘
typ ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ └─┘
423 gcd_dvd_left := assume a b, (out_dvd_iff a (associates.mk a ⊓ associates.mk b)).2 $ inf_le_left,
id ┴ ┴ └─────────┘ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ └─────────┘
src └─────────┘ └───────────┘ ┴ └───────────┘ ┴ └─────────┘
typ ┴ ┴ └─────────┘ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ └─────────┘
424 gcd_dvd_right := assume a b, (out_dvd_iff b (associates.mk a ⊓ associates.mk b)).2 $ inf_le_right,
id ┴ ┴ └─────────┘ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ └──────────┘
src └─────────┘ └───────────┘ ┴ └───────────┘ ┴ └──────────┘
typ ┴ ┴ └─────────┘ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ └──────────┘
425 dvd_gcd := assume a b c hac hab, show a ∣ (associates.mk c ⊓ associates.mk b).out,
id ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ └─┘
src ┴ └───────────┘ ┴ └───────────┘ └─┘
typ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ └─┘
426 by rw [dvd_out_iff, le_inf_iff, mk_le_mk_iff_dvd_iff, mk_le_mk_iff_dvd_iff]; exact ⟨hac, hab⟩,
id └─────────┘ └────────┘ └──────────────────┘ └──────────────────┘ └─┘ └─┘
src └──┘└─────────┘└┘└────────┘└┘└──────────────────┘└┘└──────────────────┘┴ └────┘ └┘ ┴
typ └──┘└─────────┘└┘└────────┘└┘└──────────────────┘└┘└──────────────────┘┴ └────┘ └─┘└┘└─┘┴
doc └──┘ └┘ └┘ └┘ ┴ └────┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ ┴ └────┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴ └────┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴ ┴ └┘ ┴
st └──────────────┘└──────────┘└────────────────────┘└────────────────────┘┴└────────────────┘
427 lcm_zero_left := assume a, show (⊤ ⊔ associates.mk a).out = 0, by simp,
id ┴ ┴ ┴ └───────────┘ ┴ └─┘ ┴
src ┴ ┴ └───────────┘ └─┘ ┴ └──┘
typ ┴ ┴ ┴ └───────────┘ ┴ └─┘ ┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
428 lcm_zero_right := assume a, show (associates.mk a ⊔ ⊤).out = 0, by simp,
id ┴ └───────────┘ ┴ ┴ ┴ └─┘ ┴
src └───────────┘ ┴ ┴ └─┘ ┴ └──┘
typ ┴ └───────────┘ ┴ ┴ ┴ └─┘ ┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
429 gcd_mul_lcm := assume a b,
id ┴ ┴
typ ┴ ┴
430 show (associates.mk a ⊓ associates.mk b).out * (associates.mk a ⊔ associates.mk b).out =
id └───────────┘ ┴ ┴ └───────────┘ ┴ └─┘ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ └─┘ ┴
src └───────────┘ ┴ └───────────┘ └─┘ ┴ └───────────┘ ┴ └───────────┘ └─┘ ┴
typ └───────────┘ ┴ ┴ └───────────┘ ┴ └─┘ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ └─┘ ┴
431 normalize (a * b),
id └───────┘ ┴ ┴ ┴
src └───────┘ ┴
typ └───────┘ ┴ ┴ ┴
432 by rw [← out_mk, ← out_mul, mul_comm, sup_mul_inf]; refl,
id └────┘ └─────┘ └──────┘ └─────────┘
src └────┘└────┘└──┘└─────┘└┘└──────┘└┘└─────────┘┴ └──┘
typ └────┘└────┘└──┘└─────┘└┘└──────┘└┘└─────────┘┴ └──┘
doc └────┘ └──┘ └┘ └┘ ┴ └──┘
txt └────┘ └──┘ └┘ └┘ ┴ └──┘
par └────┘ └──┘ └┘ └┘ ┴ └──┘
pid └──┘ └──┘ └┘ └┘ ┴
st └───────────┘└─────────┘└────────┘└───────────┘┴└────┘
433 normalize_gcd := assume a b, by convert normalize_out _,
id ┴ ┴ └───────────┘
src └──────┘└───────────┘└┘
typ ┴ ┴ └──────┘└───────────┘└┘
doc └──────┘ └┘
txt └──────┘ └┘
par └──────┘ └┘
pid ┴ └┘
st └──────────────────────┘
434 .. ‹normalization_domain α› }
id ┴└──────────────────┘ ┴┴
src ┴└──────────────────┘ ┴
typ ┴└──────────────────┘ ┴┴
doc ┴└──────────────────┘ ┴
435
436 end